real): generalize 'compact_space I' to 'compact_space (Icc a b)' (#6523)

Commit

4 years ago

feat(topology/instances/real): generalize 'compact_space I' to 'compact_space (Icc a b)' (#6523) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

2f357794

mathlib d7fa1bc8 - feat(topology/instances/real): generalize 'compact_space I' to 'compact_space (Icc a b)' (#6523)

mathlib
d7fa1bc8 - feat(topology/instances/real): generalize 'compact_space I' to 'compact_space (Icc a b)' (#6523)