Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-15 15:47 4a7103dd

View on Github →

refactor(topology/uniform_space): proof simplification / extension

Estimated changes

Modified analysis/metric_space.lean

deleted theorem lebesgue_number_lemma

added theorem lebesgue_number_lemma_of_metric

added theorem lebesgue_number_lemma_of_metric_sUnion

Modified analysis/topology/uniform_space.lean

deleted theorem assoc_comp_rel

added theorem comp_rel_assoc

deleted theorem lebesgue_entourage_lemma

added theorem lebesgue_number_lemma

added theorem lebesgue_number_lemma_sUnion