eqOn_Ioc_of_ae_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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