mathlib3
3b5edd06 - refactor(set_theory/cardinal_ordinal): use TC assumptions instead of inequalities (#10313)

Commit

4 years ago

refactor(set_theory/cardinal_ordinal): use TC assumptions instead of inequalities (#10313) Assume `[fintype α]` or `[infinite α]` instead of `#α < ω` or `ω ≤ #α`.

Author

urkud

Parents

d8c87253

mathlib3 3b5edd06 - refactor(set_theory/cardinal_ordinal): use TC assumptions instead of inequalities (#10313)

mathlib3
3b5edd06 - refactor(set_theory/cardinal_ordinal): use TC assumptions instead of inequalities (#10313)