Theorem Cardinal.mk_iUnion_Ordinal_le_of_le

Modification history

2026-02-02 02:01
Mathlib/SetTheory/Cardinal/Ordinal.lean
chore: rename `mk_iUnion_Ordinal_le_of_le` → `mk_biUnion_le_of_le` (#34452) …
Deleted Cardinal.mk_iUnion_Ordinal_le_of_leView on Github →
2025-03-17 11:54
Mathlib/SetTheory/Cardinal/Arithmetic.lean
refactor(SetTheory/Cardinal/Ordinal): move results (#21857) …
Modified Cardinal.mk_iUnion_Ordinal_le_of_leView on Github →
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_le_of_leView on Github →