Commit 2026-02-23 18:16 abd0739b

View on Github →

feat(SetTheory/Cardinal): more lemmas about ENat (#33909) and deduplicate a few pairs. From ProofBench

Estimated changes

added theorem Set.encard_lt_one
deleted theorem Cardinal.three_le
added theorem Cardinal.one_le_toENat
added theorem Cardinal.one_lt_toENat
deleted theorem Cardinal.toENat_eq_nat
modified theorem Cardinal.toENat_eq_ofNat
modified theorem Cardinal.toENat_eq_one
modified theorem Cardinal.toENat_eq_top
modified theorem Cardinal.toENat_eq_zero
deleted theorem Cardinal.toENat_le_nat
modified theorem Cardinal.toENat_le_ofNat
modified theorem Cardinal.toENat_le_one
modified theorem Cardinal.toENat_lift
added theorem Cardinal.toENat_lt_one
modified theorem Cardinal.toENat_lt_top
modified theorem Cardinal.toENat_ne_top
added theorem Cardinal.toENat_ofNat