thickenedIndicatorAux_one — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem thickenedIndicatorAux_one (δ : ℝ) (E : Set α) {x : α} (x_in_E : x ∈ E) : thickenedIndicatorAux δ E x = 1 := by
  simp [thickenedIndicatorAux, infEdist_zero_of_mem x_in_E, tsub_zero]

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