cardinal_measurableSet_le — Mathlib

English

The collection of measurable sets with respect to generateFrom(s) has cardinality at most max(|s|, 2^{ℵ0}).

Русский

Множество измеримых множеств относительно generateFrom(s) имеет кардинальность не более max(|s|, 2^{ℵ0}).

LaTeX

$$$\\left|\\{ t \\mid @MeasurableSet α (generateFrom(s))\, t \\} \\right| \\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_measurableSet_le (s : Set (Set α)) : #{t | @MeasurableSet α (generateFrom s) t} ≤ max (#s) 2 ^ ℵ₀ :=
  cardinal_generateMeasurable_le s

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