Mathlib Changelog
v3
Changelog
About
Github
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