thickenedIndicator_le_one — Mathlib

English

For any δ > 0 and E, the function thickenedIndicator δ_pos E x is ≤ 1 for all x.

Русский

Для любого δ > 0 и любого E функция thickenedIndicator δ_pos E x не превосходит 1 для всех x.

LaTeX

$$$\forall δ>0,\; E\subseteq \alpha:\; \operatorname{thickenedIndicator}(δ,E)(x) \le 1 \text{ for all } x$$$

Lean4

theorem thickenedIndicator_le_one {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) (x : α) : thickenedIndicator δ_pos E x ≤ 1 :=
  by
  rw [thickenedIndicator.coeFn_eq_comp]
  simpa using (toNNReal_le_toNNReal (by finiteness) one_ne_top).mpr (thickenedIndicatorAux_le_one δ E x)

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