thickenedIndicator_one — Mathlib

English

For δ > 0, E, thickenedIndicator δ E x = 1 whenever x ∈ E.

Русский

Для δ > 0 и x ∈ E выполняется thickenedIndicator δ E x = 1.

LaTeX

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

Lean4

theorem thickenedIndicator_one {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α} (x_in_E : x ∈ E) :
    thickenedIndicator δ_pos E x = 1 :=
  thickenedIndicator_one_of_mem_closure _ _ (subset_closure x_in_E)

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