eq_of_ae_eq — Mathlib

English

If f and g are continuous, then f =ᵐ[μ] g if and only if f = g.

Русский

Если f и g непрерывны, то f =ᵐ[μ] g эквивалентно f = g.

LaTeX

$$$\\forall f,g:\\ X\\to Y,\\; (Continuous f)\\land(Continuous g)\\Rightarrow (f =^{\\mu}_{ae} g) \\iff f=g.$$$

Lean4

/-- If two continuous functions are a.e. equal, then they are equal. -/
theorem eq_of_ae_eq {f g : X → Y} (h : f =ᵐ[μ] g) (hf : Continuous f) (hg : Continuous g) : f = g :=
  suffices EqOn f g univ from funext fun _ => this trivial
  eqOn_open_of_ae_eq (ae_restrict_of_ae h) isOpen_univ hf.continuousOn hg.continuousOn

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