mathlib3
f5c9d0f4 - feat(topology/algebra/ordered): generalize `real.compact_Icc` (#6602)

Commit
5 years ago
feat(topology/algebra/ordered): generalize `real.compact_Icc` (#6602) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Author
Parents
Loading