Theorem Cardinal.mk_iUnion_Ordinal_lift_le_of_le

Modification history

2024-11-14 01:17

Mathlib/SetTheory/Cardinal/Arithmetic.lean

feat(SetTheory/Cardinal/Arithmetic): fix namespace of `mk_iUnion_Ordinal_le_of_le` (#18541) …

Added Cardinal.mk_iUnion_Ordinal_lift_le_of_le View on Github →