Theorem Cardinal.add_le_add_iff_of_lt_aleph0

Modification history

2024-09-18 06:51

Mathlib/SetTheory/Cardinal/Ordinal.lean

chore(SetTheory/Cardinal/Basic): `Cardinal.IsLimit` → `IsSuccLimit` (#16899)

Modified Cardinal.add_le_add_iff_of_lt_aleph0 View on Github →

2023-02-23 13:50

Mathlib/SetTheory/Cardinal/Ordinal.lean

feat: port SetTheory.Cardinal.Ordinal (#2463)

Added Cardinal.add_le_add_iff_of_lt_aleph0 View on Github →