eqOn_Ico_of_ae_eq — Mathlib

English

If f and g are a.e. equal on Ico a b and continuous on Ico a b, then they are equal on Ico a b.

Русский

Если f и g равны почти повсюду на Ico a b и непрерывны на Ico a b, то они равны на Ico a b.

LaTeX

$$$(f =^{\\mu.restrict (Ico a b)} g) \\land (ContinuousOn f (Ico a b)) \\land (ContinuousOn g (Ico a b)) \\Rightarrow (EqOn f g (Ico a b)).$$$

Lean4

theorem eqOn_Ico_of_ae_eq [DenselyOrdered X] {a b : X} {f g : X → Y} (hfg : f =ᵐ[μ.restrict (Ico a b)] g)
    (hf : ContinuousOn f (Ico a b)) (hg : ContinuousOn g (Ico a b)) : EqOn f g (Ico a b) :=
  eqOn_of_ae_eq hfg hf hg (Ico_subset_closure_interior _ _)

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