feat(topology/metric_space/hausdorff_distance): Thickening a compact …

…inside an open (#14926)

If a compact set is contained in an open set, then we can find a (closed) thickening of it still contained in the open.

src/topology/metric_space/hausdorff_distance.lean

@@ -1065,6 +1065,18 @@ begin
     exact (cthickening_subset_thickening' hδ (half_lt_self hδ) _),
 end
 
+lemma _root_.is_compact.exists_thickening_subset_open (hs : is_compact s) (ht : is_open t)
+  (hst : s ⊆ t) :
+  ∃ δ, 0 < δ ∧ thickening δ s ⊆ t :=
+(hst.disjoint_compl_right.exists_thickenings hs ht.is_closed_compl).imp $ λ δ h,
+  ⟨h.1, disjoint_compl_right_iff_subset.1 $ h.2.mono_right $ self_subset_thickening h.1 _⟩
+
+lemma _root_.is_compact.exists_cthickening_subset_open (hs : is_compact s) (ht : is_open t)
+  (hst : s ⊆ t) :
+  ∃ δ, 0 < δ ∧ cthickening δ s ⊆ t :=
+(hst.disjoint_compl_right.exists_cthickenings hs ht.is_closed_compl).imp $ λ δ h,
+  ⟨h.1, disjoint_compl_right_iff_subset.1 $ h.2.mono_right $ self_subset_cthickening _⟩
+
 lemma cthickening_eq_Inter_cthickening' {δ : ℝ}
   (s : set ℝ) (hsδ : s ⊆ Ioi δ) (hs : ∀ ε, δ < ε → (s ∩ (Ioc δ ε)).nonempty) (E : set α) :
   cthickening δ E = ⋂ ε ∈ s, cthickening ε E :=