ae_eq_iff_eq — Mathlib

English

If a.e. equality on an open set holds for f and g, and f,g are continuous on that set, then they are equal on that set.

Русский

Если f и g равны почти повсюду на открытом множестве и оба непрерывны на этом множестве, то они равны на этом множестве.

LaTeX

$$$\\forall {X,Y},\\; (MeasureTheory.ae (μ.restrict U)).EventuallyEq f g \\rightarrow IsOpen U \\rightarrow ContinuousOn f U \\rightarrow ContinuousOn g U \\rightarrow Set.EqOn f g U.$$$

Lean4

theorem _root_.Continuous.ae_eq_iff_eq {f g : X → Y} (hf : Continuous f) (hg : Continuous g) : f =ᵐ[μ] g ↔ f = g :=
  ⟨fun h => eq_of_ae_eq h hf hg, fun h => h ▸ EventuallyEq.rfl⟩

Похожие утверждения