English
For any nonassociative semiring, doubling a element equals adding the element to itself: n + n = 2 · n.
Русский
В любой неассоциативной полукольце удвоение элемента равно сложению элемента с самим собой: n + n = 2n.
LaTeX
$$$ a + a = 2 \cdot a \quad\text{for every } a$$$
Lean4
/-- If the indicators of measurable sets `Aᵢ` tend pointwise to the indicator of a set `A`
and we eventually have `Aᵢ ⊆ B` for some set `B` of finite measure, then the measures of `Aᵢ`
tend to the measure of `A`. -/
theorem tendsto_measure_of_tendsto_indicator {μ : Measure α} (As_mble : ∀ i, MeasurableSet (As i)) {B : Set α}
(B_mble : MeasurableSet B) (B_finmeas : μ B ≠ ∞) (As_le_B : ∀ᶠ i in L, As i ⊆ B)
(h_lim : ∀ x, ∀ᶠ i in L, x ∈ As i ↔ x ∈ A) : Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A)) :=
by
rcases L.eq_or_neBot with rfl | _
· exact tendsto_bot
apply tendsto_measure_of_ae_tendsto_indicator L ?_ As_mble B_mble B_finmeas As_le_B (ae_of_all μ h_lim)
exact measurableSet_of_tendsto_indicator L As_mble h_lim
