compl_mem_cofinite — Mathlib

English

For any subset s of α, the complement s^c lies in the cofinite σ-algebra μ.cofinite if and only if μ(s) is finite. Equivalently, μ(s) < ∞ ⇔ s^c ∈ μ.cofinite.

Русский

Для произвольного подмножества s множества α комплемент s^c принадлежит кофинитной сигма-алгебе μ.cofinite тогда и только тогда, когда мера μ среды s есть конечна. Эквивалентно μ(s) < ∞ ⇔ s^c ∈ μ.cofinite.

LaTeX

$$$s^{\mathrm{c}} \in \mu\mathrm{.cofinite} \;\iff\; \mu(s) < \infty$$$

Lean4

theorem compl_mem_cofinite : sᶜ ∈ μ.cofinite ↔ μ s < ∞ := by rw [mem_cofinite, compl_compl]

Похожие утверждения