cardinal_generateMeasurable_le — Mathlib

English

The sigma-algebra generated by s has cardinality at most max(|s|, 2^{ℵ0}).

Русский

σ-алгебра, порождаемая s, имеет кардинальность не более max(|s|, 2^{ℵ0}).

LaTeX

$$$\\#\\{t \\mid GenerateMeasurable(s,t)\\} \\le \\max\\big(\\#s, 2^{\\aleph_0}\\big)$$

Lean4

/-- If a sigma-algebra is generated by a set of sets `s`, then the sigma-algebra has cardinality at
most `max #s 2 ^ ℵ₀`. -/
theorem cardinal_generateMeasurable_le (s : Set (Set α)) : #{t | GenerateMeasurable s t} ≤ max (#s) 2 ^ ℵ₀ :=
  by
  rw [generateMeasurable_eq_rec.{u, 0}]
  exact cardinal_generateMeasurableRec_le s _

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