Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-03 08:02 7c2ce0c2

View on Github →

refactor(set_theory/cardinal/basic): redefine cardinal.is_limit in terms of is_succ_limit (#18523) We redefine cardinal.is_limit x as x ≠ 0 ∧ is_succ_limit x. This will allow us to make use of the extensive is_succ_limit API in the future.

Estimated changes

deleted theorem cardinal.is_limit.ne_zero
deleted theorem cardinal.is_limit.succ_lt
deleted def cardinal.is_limit
deleted theorem cardinal.is_limit_aleph_0
modified theorem cardinal.aleph'_limit
modified theorem cardinal.aleph_limit
modified theorem cardinal.beth_limit
modified theorem cardinal.ord_aleph_is_limit