English
If indicator functions converge almost everywhere to the indicator of A along a nontrivial countably generated filter, then A is a.e.-measurable.
Русский
Если индикаторные функции сходятся почти повсюду к индикатору A вдоль ненулевого счѐтывающего фильтра, то A является а.е.-измеримым.
LaTeX
$$$\\text{NullMeasurableSet}(A, \\mu)$$$
Lean4
/-- If the indicator functions of a.e.-measurable sets `Aᵢ` converge a.e. to the indicator function
of a set `A` along a nontrivial countably generated filter, then `A` is also a.e.-measurable. -/
theorem nullMeasurableSet_of_tendsto_indicator [NeBot L] {μ : Measure α} (As_mble : ∀ i, NullMeasurableSet (As i) μ)
(h_lim : ∀ᵐ x ∂μ, ∀ᶠ i in L, x ∈ As i ↔ x ∈ A) : NullMeasurableSet A μ :=
by
simp_rw [← aemeasurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢
apply aemeasurable_of_tendsto_metrizable_ae L As_mble
simpa [tendsto_indicator_const_apply_iff_eventually] using h_lim
