frontier_thickening_disjoint — Mathlib

English

Radii produce pairwise disjoint frontiers: frontiers of thickening at distinct radii are pairwise disjoint.

Русский

Радиусы порождают попарно непересекающиеся фронтиры: фронтиры thickening при различных радиусах попарно не пересекаются.

LaTeX

$$Pairwise (Disjoint on fun r : ℝ => frontier (thickening r A))$$

Lean4

theorem frontier_thickening_disjoint (A : Set α) : Pairwise (Disjoint on fun r : ℝ => frontier (thickening r A)) :=
  by
  refine (pairwise_disjoint_on _).2 fun r₁ r₂ hr => ?_
  rcases le_total r₁ 0 with h₁ | h₁
  · simp [thickening_of_nonpos h₁]
  refine
    ((disjoint_singleton.2 fun h => hr.ne ?_).preimage _).mono (frontier_thickening_subset _)
      (frontier_thickening_subset _)
  apply_fun ENNReal.toReal at h
  rwa [ENNReal.toReal_ofReal h₁, ENNReal.toReal_ofReal (h₁.trans hr.le)] at h

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