Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-17 23:10 4299a801

View on Github →

refactor(topology/subset_properties): use finite subcovers indexed by types (#1980)

wip
wip
wip
wip
WIP
WIP
Reset changes that belong to other PR
Docstrings
Add Heine--Borel to docstring
Cantor's intersection theorem
Cantor for sequences
Generalise Cantor intersection thm
More fixes

Estimated changes

Modified src/topology/metric_space/basic.lean

Modified src/topology/subset_properties.lean

modified theorem compact.elim_finite_subcover

added theorem compact.elim_finite_subfamily_closed

added theorem compact.nonempty_Inter_of_directed_nonempty_compact_closed

added theorem compact.nonempty_Inter_of_sequence_nonempty_compact_closed

added theorem compact_iff_finite_subfamily_closed

added theorem compact_of_finite_subfamily_closed

added theorem compact_space_of_finite_subfamily_closed

modified theorem set.finite.compact_bUnion