Commit 2024-10-16 12:56 d03e389c

View on Github →

feat(SetTheory/Ordinal/Enum): more lemmas on enumOrd (#17668)

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem ciInf_eq_bot_of_bot_mem

added theorem ciInf_eq_top_of_top_mem

added theorem csInf_eq_bot_of_bot_mem

added theorem csSup_eq_top_of_top_mem

Modified Mathlib/SetTheory/Ordinal/Enum.lean

added theorem Ordinal.enumOrd_inj

added theorem Ordinal.enumOrd_injective

added theorem Ordinal.enumOrd_le_enumOrd

added theorem Ordinal.enumOrd_lt_enumOrd

added theorem Ordinal.id_le_enumOrd

added theorem Ordinal.le_enumOrd_self