frontier_cthickening_disjoint — Mathlib

English

For any set A, the family of frontiers frontier(cthickening r A) for r≥0 are pairwise disjoint as r varies over ℝ≥0.

Русский

Для множества A границы frontier(cthickening r A) при разных r≥0 попарно не пересекаются.

LaTeX

$$Pairwise (Disjoint on fun r : ℝ≥0 => frontier (cthickening r A))$$

Lean4

theorem frontier_cthickening_disjoint (A : Set α) : Pairwise (Disjoint on fun r : ℝ≥0 => frontier (cthickening r A)) :=
  fun r₁ r₂ hr =>
  ((disjoint_singleton.2 <| by simpa).preimage _).mono (frontier_cthickening_subset _) (frontier_cthickening_subset _)

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