Commit 2021-10-05 21:57 fdf8a71f

View on Github →

feat(topology/bases): a family of nonempty disjoint open sets is countable in a separable space (#9557) Together with unrelated small lemmas on balls and on pairwise_on.

Estimated changes

Modified src/analysis/normed_space/riesz_lemma.lean

Modified src/data/real/ennreal.lean

added theorem ennreal.exists_le_of_sum_le

added theorem ennreal.sum_lt_sum_of_nonempty

Modified src/data/set/basic.lean

added theorem set.pairwise_on_disjoint_on_mono

Modified src/data/set/lattice.lean

added theorem set.pairwise_on_Union

Modified src/measure_theory/constructions/borel_space.lean

Modified src/topology/bases.lean

added theorem topological_space.countable_of_is_open_of_disjoint

added theorem topological_space.countable_of_nonempty_interior_of_disjoint

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem emetric.disjoint_closed_ball_of_lt_inf_edist

added theorem is_closed.Hausdorff_dist_zero_iff_eq

added theorem is_closed.mem_iff_inf_dist_zero

added theorem is_closed.not_mem_iff_inf_dist_pos

deleted theorem metric.Hausdorff_dist_zero_iff_eq_of_closed

added theorem metric.disjoint_closed_ball_of_lt_inf_dist

deleted theorem metric.mem_iff_inf_dist_zero_of_closed