sequence_le — Mathlib

English

For every a ∈ α, the f-value at index encode(a) + 1 is bounded above by f(a): f(hf.sequence f (encode(a) + 1)) ≤ f(a).

Русский

Для каждого a ∈ α значение f на позиции encode(a) + 1 не превышает f(a): f(hf.sequence f(encode(a) + 1)) ≤ f(a).

LaTeX

$$$ f\\big(hf.sequence\\,f(\\operatorname{encode}(a) + 1)\\big) \\le f(a). $$$

Lean4

theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f a :=
  hf.rel_sequence a

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