thickenedIndicatorAux_one_of_mem_closure

English

If x ∈ closure E, then thickenedIndicatorAux δ E x = 1 for any δ ∈ ℝ.

Русский

Если x ∈ closure E, то для любого δ ∈ ℝ выполняется thickenedIndicatorAux δ E x = 1.

LaTeX

$$$\forall \delta \in \mathbb{R},\; \forall E \subseteq \alpha,\; \forall x \in \overline{E}:\; \operatorname{thickenedIndicatorAux}(\delta,E)(x) = 1$$$

Lean4

theorem thickenedIndicatorAux_one_of_mem_closure (δ : ℝ) (E : Set α) {x : α} (x_mem : x ∈ closure E) :
    thickenedIndicatorAux δ E x = 1 := by
  rw [← thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_one δ (closure E) x_mem]

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