Theorem MeasurableSpace.generateMeasurableRec_of_omega_one_le

Modification history

2025-12-22 18:39
Mathlib/MeasureTheory/MeasurableSpace/Card.lean
refactor: standardize spelling of `ℵ₁` as `aleph_one` (#33198) …
Added MeasurableSpace.generateMeasurableRec_of_omega_one_leView on Github →