mathlib
64c8d217 - feat(set_theory/ordinal): `Inf_empty` (#12226)

Commit

4 years ago

feat(set_theory/ordinal): `Inf_empty` (#12226) The docs mention that `Inf Ø` is defined as `0`. We prove that this is indeed the case.

Author

vihdzp

Parents