subset_compl_thickening_compl_thickening_self

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

Похожие утверждения