Commit 2026-01-21 17:08 d630389c

View on Github →

chore(SetTheory/Cardinal): remove explicit argument to nat_lt_aleph0 (#33990) It is almost never used. Also rename to natCast_lt_aleph0 and add natCast_le_aleph0.

Estimated changes

modified theorem Cardinal.aleph0_le
deleted theorem Cardinal.nat_lt_aleph0
modified theorem Cardinal.one_lt_aleph0
modified theorem Cardinal.nat_lt_univ