cardinal_generateMeasurable_le_continuum

English

If the generator s has cardinality at most the continuum, then the generated sigma-algebra also has cardinality at most the continuum.

Русский

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

LaTeX

$$\\#s \\le \\mathfrak{c} \\Rightarrow \\#\\{t \\mid GenerateMeasurable s t\\} \\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_generateMeasurable_le_continuum {s : Set (Set α)} (hs : #s ≤ 𝔠) : #{t | GenerateMeasurable s t} ≤ 𝔠 :=
  by
  apply (cardinal_generateMeasurable_le s).trans
  rw [← continuum_power_aleph0]
  exact_mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le)

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