English
A family of indicatorConstLp functions is continuous in the parameter if μ(t_b Δ s) → 0 as b → x; then indicatorConstLp converges to indicatorConstLp(p, hs, hμs, c).
Русский
Семейство indicatorConstLp непрерывно по параметру при сходящемся к нулю мерам симм. разности; индикатор сходится к пределу.
LaTeX
$$$\text{tendsto indicatorConstLp set lemma: }$ (informal) $$\lim_{b\to x} indicatorConstLp(p,ht_b, hμt_b,c) = indicatorConstLp(p, hs, hμs, c).$$$$
Lean4
theorem dist_indicatorConstLp_eq_norm {t : Set α} {ht : MeasurableSet t} {hμt : μ t ≠ ∞} :
dist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) =
‖indicatorConstLp p (hs.symmDiff ht) (measure_symmDiff_ne_top hμs hμt) c‖ :=
by
-- Squeezed for performance reasons
simp only [Lp.dist_edist, edist_indicatorConstLp_eq_enorm, enorm, ENNReal.coe_toReal, Lp.coe_nnnorm]