Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-11 17:09 f5c9d0f4

View on Github →

feat(topology/algebra/ordered): generalize real.compact_Icc (#6602)

Estimated changes

Modified src/data/set/intervals/basic.lean

added theorem set.Icc_bot_top

Modified src/order/filter/ultrafilter.lean

added theorem ultrafilter.diff_mem_iff

Modified src/topology/algebra/ordered.lean

added theorem compact_Icc

added theorem compact_interval

added theorem compact_pi_Icc

Modified src/topology/instances/real.lean

deleted theorem compact_Icc

deleted theorem compact_pi_Icc

deleted theorem real.totally_bounded_Icc

deleted theorem real.totally_bounded_Ico

deleted theorem real.totally_bounded_Ioo

Modified src/topology/metric_space/basic.lean

added theorem totally_bounded_Icc

added theorem totally_bounded_Ico

added theorem totally_bounded_Ioc

added theorem totally_bounded_Ioo

Modified src/topology/uniform_space/cauchy.lean

added theorem is_compact.is_complete

added theorem is_compact.totally_bounded