Commit 2021-03-10 02:23 4e370b5d

feat(topology): shrinking lemma (#6478)

Add a few versions of the shrinking lemma:

• exists_subset_Union_closure_subset and exists_Union_eq_closure_subset: shrinking lemma for general normal spaces;
• exists_subset_Union_ball_radius_lt, exists_Union_ball_eq_radius_lt, exists_subset_Union_ball_radius_pos_lt, exists_Union_ball_eq_radius_pos_lt: shrinking lemma for coverings by open balls in a proper metric space;
• exists_locally_finite_subset_Union_ball_radius_lt, exists_locally_finite_Union_eq_ball_radius_lt: given a positive function R : X → ℝ, finds a locally finite covering by open balls ball (c i) (r' i), r' i < R and a subcovering by balls of strictly smaller radius ball (c i) (r i), 0 < r i < r' i.

Other API changes

• add @[simp] to set.compl_subset_compl;
• add is_closed_bInter and locally_finite.point_finite;
• add metric.closed_ball_subset_closed_ball, metric.uniformity_basis_dist_lt, exists_pos_lt_subset_ball, and exists_lt_subset_ball;
• generalize refinement_of_locally_compact_sigma_compact_of_nhds_basis to refinement_of_locally_compact_sigma_compact_of_nhds_basis_set, replace arguments (s : X → set X) (hs : ∀ x, s x ∈ 𝓝 x) with a hint to use filter.has_basis.restrict_subset if needed.
• make s and t arguments of normal_separation implicit;
• add normal_exists_closure_subset;
• turn sigma_compact_space_of_locally_compact_second_countable into an instance.