frontier_thickening_subset — Mathlib

English

For nonempty X and E ⊆ X, x ∈ thickening δ E iff ∃ z ∈ E such that edist x z < δ.

Русский

Для непустого E ⊆ X верно: x ∈ thickening δ E тогда и только тогда, существуют z ∈ E с edist x z < δ.

LaTeX

$$$x ∈ thickening\\,δ\\,E \\iff ∃ z ∈ E, edist\\,x\\,z < ENNReal.ofReal\\,δ$$$

Lean4

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

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