eqOn_of_ae_eq — Mathlib

English

If two continuous functions are a.e. equal on an open set then they are equal on that open set.

Русский

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

LaTeX

$$${\\text{EqOn f g U}}$ при условии, что U открыто, f,g непрерывны на U и f =ᵐ[μ\\restriction U] g.$$

Lean4

theorem eqOn_of_ae_eq {f g : X → Y} (h : f =ᵐ[μ.restrict s] g) (hf : ContinuousOn f s) (hg : ContinuousOn g s)
    (hU : s ⊆ closure (interior s)) : EqOn f g s :=
  have : interior s ⊆ s := interior_subset
  (eqOn_open_of_ae_eq (ae_restrict_of_ae_restrict_of_subset this h) isOpen_interior (hf.mono this)
        (hg.mono this)).of_subset_closure
    hf hg this hU

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