mathlib3
e08a42b2 - chore(set_theory/cardinal/basic): missing lemmas about `lift c < ℵ₀` and `ℵ₀ < lift c` (#18746)

Commit
2 years ago
chore(set_theory/cardinal/basic): missing lemmas about `lift c < ℵ₀` and `ℵ₀ < lift c` (#18746) We already had the `le` versions `lift_le_aleph0` and `aleph0_le_lift`, this adds the `lt` ones `lift_lt_aleph0` and `aleph0_lt_lift`. This turns out to be useful for proving some results about `finrank`, as well as golfing some existing proofs. Since they're trivial, this adds the same lemmas about `continuum` too.
Author
Parents
Loading