thickenedIndicator_zero — Mathlib

English

If x ∉ thickening δ E, then thickenedIndicator δ E x = 0.

Русский

Если x не принадлежит δ-толщению E, тогда thickenedIndicator δ E x = 0.

LaTeX

$$$\forall δ \in \mathbb{R}, δ>0,\; E:\; x \notin \operatorname{thickening}(δ,E)\Rightarrow \operatorname{thickenedIndicator}(δ,E)(x) = 0$$$

Lean4

theorem thickenedIndicator_zero {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α} (x_out : x ∉ thickening δ E) :
    thickenedIndicator δ_pos E x = 0 := by
  rw [thickenedIndicator_apply, thickenedIndicatorAux_zero δ_pos E x_out, toNNReal_zero]

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