`BookProof.ChapterGaugeParametrization.isPhysicalObservable_iff_factors_through` (π : X → Y) (f : X → ℝ) : IsPhysicalObservable (fiberGauge π) f ↔ ∃ F : Y → ℝ, ∀ x, f x = F (π x)

Initializing...

`BookProof.ChapterGaugeParametrization.isPhysicalObservable_iff_factors_through` (π : X → Y) (f : X → ℝ) : IsPhysicalObservable (fiberGauge π) f ↔ ∃ F : Y → ℝ, ∀ x, f x = F (π x) · Prove2Me