thickenedIndicator_one_of_mem_closure

English

If x ∈ closure E, then thickenedIndicator δ_pos E x = 1.

Русский

Если x ∈ closure E, то thickenedIndicator δ_pos E x = 1.

LaTeX

$$$\forall δ>0,\; E \subseteq \alpha:\; x \in \overline{E} \Rightarrow \operatorname{thickenedIndicator}(δ,E)(x) = 1$$$

Lean4

theorem thickenedIndicator_one_of_mem_closure {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α} (x_mem : x ∈ closure E) :
    thickenedIndicator δ_pos E x = 1 := by
  rw [thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure δ E x_mem, toNNReal_one]

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