sep_infinite — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sep_infinite [Countable α] {S : Set (Set α)} (hS : MeasurableSet S) : MeasurableSet ({s ∈ S | s.Infinite}) :=
  hS.inter .setOf_infinite

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