Commit 2026-02-02 02:01 20310f50

View on Github →

chore: rename mk_iUnion_Ordinal_le_of_le → mk_biUnion_le_of_le (#34452) The former had bad capitalization, and referred to iUnion where biUnion would be more conventional.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

added theorem Cardinal.mk_biUnion_le_of_le

added theorem Cardinal.mk_biUnion_le_of_le_lift

deleted theorem Cardinal.mk_iUnion_Ordinal_le_of_le

deleted theorem Cardinal.mk_iUnion_Ordinal_lift_le_of_le