partialSups_le_iff — Mathlib

English

For f: ι → α, i: ι, a: α, we have partialSups f i ≤ a iff ∀ j ≤ i, f j ≤ a.

Русский

Для функций f: ι → α, индекса i и элемента a выполняется: partialSups f i ≤ a тогда и только тогда, когда ∀ j ≤ i, f(j) ≤ a.

LaTeX

$$$\\partialSups f i \\le a \\;\\Longleftrightarrow\\; \\forall j \\le i, \\; f(j) \\le a$$$

Lean4

@[simp]
theorem partialSups_le_iff {f : ι → α} {i : ι} {a : α} : partialSups f i ≤ a ↔ ∀ j ≤ i, f j ≤ a :=
  partialSups_iff_forall (· ≤ a) sup_le_iff

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