eqOn_Ioo_of_ae_eq — Mathlib

English

If f and g are ae-equal on Ioo a b, and continuous on Ioo a b, then they are equal on Ioo a b.

Русский

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

LaTeX

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

Lean4

theorem eqOn_Ioo_of_ae_eq {a b : X} {f g : X → Y} (hfg : f =ᵐ[μ.restrict (Ioo a b)] g) (hf : ContinuousOn f (Ioo a b))
    (hg : ContinuousOn g (Ioo a b)) : EqOn f g (Ioo a b) :=
  eqOn_of_ae_eq hfg hf hg Ioo_subset_closure_interior

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