one_le_thickenedIndicator_apply' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem one_le_thickenedIndicator_apply' {X : Type _} [PseudoEMetricSpace X] {δ : ℝ} (δ_pos : 0 < δ) {F : Set X} {x : X}
    (hxF : x ∈ closure F) : 1 ≤ thickenedIndicator δ_pos F x := by
  rw [thickenedIndicator_one_of_mem_closure δ_pos F hxF]

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