English
If the indicator functions of measurable sets converge to the indicator of a set A along a nontrivial countably generated filter, then A is measurable.
Русский
Если индикаторные функции измеримых множеств сходятся к индикатору множества A вдоль ненулевого счѐтывающего фильтра, то A измеримо.
LaTeX
$$$\\text{measurableSet}(A) = \\text{indicator- convergence}$$$
Lean4
/-- If the indicator functions of measurable sets `Aᵢ` converge to the indicator function of
a set `A` along a nontrivial countably generated filter, then `A` is also measurable. -/
theorem measurableSet_of_tendsto_indicator [NeBot L] (As_mble : ∀ i, MeasurableSet (As i))
(h_lim : ∀ x, ∀ᶠ i in L, x ∈ As i ↔ x ∈ A) : MeasurableSet A :=
by
simp_rw [← measurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢
exact
ENNReal.measurable_of_tendsto' L As_mble ((tendsto_indicator_const_iff_forall_eventually L (1 : ℝ≥0∞)).mpr h_lim)
