cardinal_measurableSet_le_continuum

English

If the generating family s has cardinality at most contiuum, the σ-algebra generated from s has cardinality at most continuum.

Русский

Если порождающее семейство s имеет кардинальность не более континуума, σ-алгебра, порожденная s, имеет кардинальность не более континуума.

LaTeX

$$$\\#s \\le \\mathfrak{c} \\Rightarrow \\#\\{ t \\mid t \\in \\text{MeasurableSet w.r.t. generateFrom}(s) \\} \\le \\mathfrak{c}$$$

Lean4

/-- If a sigma-algebra is generated by a set of sets `s` with cardinality at most the continuum,
then the sigma algebra has the same cardinality bound. -/
theorem cardinal_measurableSet_le_continuum {s : Set (Set α)} :
    #s ≤ 𝔠 → #{t | @MeasurableSet α (generateFrom s) t} ≤ 𝔠 :=
  cardinal_generateMeasurable_le_continuum

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