sep_finite — Mathlib

English

If α is countable and S is a measurable family of subsets of α, then the subfamily {s ∈ S | s.Finite} is measurable.

Русский

Пусть α счётно, S — измеримое семейство подмножеств α. Тогда множество {s ∈ S | s конечное} измеримо.

LaTeX

$$$ [Countable \alpha] {S : Set (Set \alpha)} (hS : MeasurableSet S) : MeasurableSet ({s \\in S | s.Finite}) $$$

Lean4

theorem sep_finite [Countable α] {S : Set (Set α)} (hS : MeasurableSet S) : MeasurableSet ({s ∈ S | s.Finite}) :=
  hS.inter .setOf_finite

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