Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-20 14:17 38b95c8a

View on Github →

feat(set_theory/cardinal): simp lemmas about numerals (#3450)

Estimated changes

Modified src/set_theory/cardinal.lean

modified theorem cardinal.one_lt_omega

modified theorem cardinal.zero_lt_one

Modified src/set_theory/ordinal.lean

added theorem cardinal.bit0_eq_self

added theorem cardinal.bit0_le_bit0

added theorem cardinal.bit0_le_bit1

added theorem cardinal.bit0_lt_bit0

added theorem cardinal.bit0_lt_bit1

added theorem cardinal.bit0_lt_omega

added theorem cardinal.bit0_ne_zero

added theorem cardinal.bit1_eq_self_iff

added theorem cardinal.bit1_le_bit0

added theorem cardinal.bit1_le_bit1

added theorem cardinal.bit1_lt_bit0

added theorem cardinal.bit1_lt_bit1

added theorem cardinal.bit1_lt_omega

added theorem cardinal.bit1_ne_zero

added theorem cardinal.omega_le_bit0

added theorem cardinal.omega_le_bit1

added theorem cardinal.one_le_bit0

added theorem cardinal.one_le_bit1

added theorem cardinal.one_le_one

added theorem cardinal.one_lt_bit0

added theorem cardinal.one_lt_bit1

added theorem cardinal.one_lt_two

added theorem cardinal.zero_lt_bit0

added theorem cardinal.zero_lt_bit1