English
If f and g are a.e. equal on an open set U and are continuous on U, then they are equal on U.
Русский
Если f и g равны почти повсюду на открытом множестве U и оба непрерывны на U, то они равны на U.
LaTeX
$$$\\forall f,g: X\\to Y,\\ (f =^{\\mu}_{U} g)\\text{ on }U\\text{ with }U\\text{ open} \\land f,g\\text{ continuous on }U \\Rightarrow f=g\\text{ on }U.$$$
Lean4
/-- If two functions are a.e. equal on an open set and are continuous on this set, then they are
equal on this set. -/
theorem eqOn_open_of_ae_eq {f g : X → Y} (h : f =ᵐ[μ.restrict U] g) (hU : IsOpen U) (hf : ContinuousOn f U)
(hg : ContinuousOn g U) : EqOn f g U :=
by
replace h := ae_imp_of_ae_restrict h
simp only [ae_iff, Classical.not_imp] at h
have : IsOpen (U ∩ {a | f a ≠ g a}) :=
by
refine isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) ?_
rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
exact
(hf.continuousAt (hU.mem_nhds ha)).prodMk_nhds (hg.continuousAt (hU.mem_nhds ha))
(isClosed_diagonal.isOpen_compl.mem_nhds ha')
replace := (this.eq_empty_of_measure_zero h).le
exact fun x hx => Classical.not_not.1 fun h => this ⟨hx, h⟩
