thickenedIndicatorAux_closure_eq — Mathlib

English

For any δ ∈ ℝ and any E ⊆ α, thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E.

Русский

Для любого δ ∈ ℝ и любого E ⊆ α thickenedIndicatorAux δ (closure E) равно thickenedIndicatorAux δ E.

LaTeX

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

Lean4

theorem thickenedIndicatorAux_closure_eq (δ : ℝ) (E : Set α) :
    thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E := by
  simp +unfoldPartialApp only [thickenedIndicatorAux, infEdist_closure]

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