Commit 2026-10-28 01:55 0eb5a97d

View on Github →

feat(SetTheory/Cardinal/Finite): simp lemmas for [E]Nat.card (#44408)

  • ENat.toNat (ENat.card α) = Nat.card α
  • Cardinal.toNat (Cardinal.mk α) = Nat.card α
  • Cardinal.toENat (Cardinal.mk α) = ENat.card α

Estimated changes

added theorem Set.encard_ofPred
added theorem Set.ncard_ofPred
modified theorem Set.toENat_cardinalMk
added theorem Cardinal.toENat_mk
added theorem Cardinal.toNat_mk
modified theorem ENat.card_eq_top
modified theorem ENat.card_lt_top
modified theorem ENat.card_lt_top_of_finite
added theorem ENat.toNat_card