thickenedIndicatorAux_lt_top — Mathlib

English

For every δ ∈ ℝ, every E ⊆ α, and every x ∈ α, thickenedIndicatorAux δ E x is finite; in particular it is less than ∞.

Русский

Для любых δ ∈ ℝ, любого множества E ⊆ α и любой точки x ∈ α значение thickenedIndicatorAux δ E x конечно и меньше чем ∞.

LaTeX

$$$\forall \delta \in \mathbb{R},\; E \subseteq \alpha,\; x \in \alpha:\; thickenedIndicatorAux(\delta,E)(x) < \infty$$$

Lean4

@[aesop safe (rule_sets := [finiteness])]
theorem thickenedIndicatorAux_lt_top {δ : ℝ} {E : Set α} {x : α} : thickenedIndicatorAux δ E x < ∞ :=
  lt_of_le_of_lt (thickenedIndicatorAux_le_one _ _ _) one_lt_top

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