finiteAt_principal — Mathlib

English

For any subset s, μ(s) < ∞ if and only if μ is finite on the principal filter generated by s.

Русский

Для любого множества s мера μ(m) конечна тогда и только тогда, когда μ конечна на главном фильтре, порожденном s.

LaTeX

$$$$\mu(s) < \infty \quad\Leftrightarrow\quad \mu \text{ is finite on } \mathcal{P}(s) \text{ (principal filter)}.$$$$

Lean4

@[simp]
theorem finiteAt_principal : μ.FiniteAtFilter (𝓟 s) ↔ μ s < ∞ :=
  ⟨fun ⟨_t, ht, hμ⟩ => (measure_mono ht).trans_lt hμ, fun h => ⟨s, mem_principal_self s, h⟩⟩

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