eqOn_Icc_of_ae_eq — Mathlib

English

If a ≠ b and f,g are a.e. equal on Icc a b and continuous on Icc a b, then EqOn f g on Icc a b.

Русский

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

LaTeX

$$$hne: a \\neq b \\rightarrow \\forall f,g: X\\to Y,\\ (f =^{\\mu.restrict (Icc a b)} g) \\land (ContinuousOn f (Icc a b)) \\land (ContinuousOn g (Icc a b)) \\Rightarrow EqOn f g (Icc a b).$$$

Lean4

theorem eqOn_Icc_of_ae_eq [DenselyOrdered X] {a b : X} (hne : a ≠ b) {f g : X → Y} (hfg : f =ᵐ[μ.restrict (Icc a b)] g)
    (hf : ContinuousOn f (Icc a b)) (hg : ContinuousOn g (Icc a b)) : EqOn f g (Icc a b) :=
  eqOn_of_ae_eq hfg hf hg (closure_interior_Icc hne).symm.subset

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