English
The frontier of thickening δ E for different δ are disjoint as a family.
Русский
Фронтиры thickening δ E при разных δ образуют попарно непересекающееся семейство.
LaTeX
$$Pairwise (Disjoint on fun δ => frontier (thickening δ E))$$
Lean4
/-- Any set is contained in the complement of the δ-thickening of the complement of its
δ-thickening. -/
theorem subset_compl_thickening_compl_thickening_self (δ : ℝ) (E : Set α) : E ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ :=
by
intro x x_in_E
simp only [thickening, mem_compl_iff, mem_setOf_eq, not_lt]
apply EMetric.le_infEdist.mpr fun y hy ↦ ?_
simp only [mem_compl_iff, mem_setOf_eq, not_lt] at hy
simpa only [edist_comm] using le_trans hy <| EMetric.infEdist_le_edist_of_mem x_in_E