Commit 2024-11-14 01:17 bc258ebb
View on Github →feat(SetTheory/Cardinal/Arithmetic): fix namespace of mk_iUnion_Ordinal_le_of_le (#18541)
This was previously in the Ordinal.Cardinal namespace, it's now been moved to simply the Cardinal namespace.
Also add the universe-polymorphic version of this lemma.