Continuity of measures of moving sets in Mathlib: ae indicator convergence

To prove that x ↦ μ (S x) is continuous when the sets move with x (half-planes {a·p < c}, intervals Ioc (a x) (b x)), use MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure (in Mathlib.MeasureTheory.Integral.Indicator). The only hypothesis is ∀ᵐ t, ∀ᶠ x in 𝓝 x₀, (t ∈ S x ↔ t ∈ S x₀). Discharge it with measure_mono_null into the boundary of S x₀ (a line, or {a x₀, b x₀}; null by an assumption or by (toFinite _).measure_zero μ under NullSingletonClass; NoAtoms is deprecated in v4.35). Off the boundary every defining inequality is strict, so ContinuousAt.eventually_lt keeps it for nearby x. Then compose with ENNReal.tendsto_toReal (measure_ne_top μ S₀), and name the set explicitly, because ContinuousAt.comp otherwise unifies the inner function with ⇑μ. For sign(u x)·m x with m = 0 where u = 0, prove continuity at points with u x₀ = 0 with squeeze_zero_norm against ‖m‖.