frontier_cthickening_subset — Mathlib

English

The frontier (boundary) of the closed thickening of E is contained in the level set {x : infEdist(x,E) = ENNReal.ofReal δ}.

Русский

Граница замкнутого уплотнения E содержится в множествах, где инф. расстояние до E равно δ.

LaTeX

$$$\operatorname{frontier}(\operatorname{cthickening}_{\delta} E) \subseteq \{x : \operatorname{infEdist}(x,E) = \operatorname{ENNReal.ofReal}(\delta)\}$$$

Lean4

/-- The frontier of the closed thickening of a set is contained in an `EMetric.infEdist` level
set. -/
theorem frontier_cthickening_subset (E : Set α) {δ : ℝ} :
    frontier (cthickening δ E) ⊆ {x : α | infEdist x E = ENNReal.ofReal δ} :=
  frontier_le_subset_eq continuous_infEdist continuous_const

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