mathlib
7a5d15a9 - feat(data/pnat/interval): Finite intervals in ℕ+ (#9534)

Commit
4 years ago
feat(data/pnat/interval): Finite intervals in ℕ+ (#9534) This proves that `ℕ+` is a locally finite order.
Author
Parents
Loading