Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 09:39 62538c8c

View on Github →

feat(analysis/metric_spaces): Compact and proper spaces (#430)

Estimated changes

Modified analysis/metric_space.lean

added theorem ball_subset_closed_ball

added theorem countable_closure_of_compact

added theorem finite_cover_balls_of_compact

added theorem mem_closure_iff'

added theorem second_countable_of_separable_metric_space

Modified analysis/topology/continuity.lean

added theorem compact_univ

deleted theorem locally_compact_of_compact

Modified analysis/topology/uniform_space.lean

added theorem complete_of_compact_set

Modified data/real/basic.lean

added theorem real.le_of_forall_epsilon_le