iSup_lt_iff — Mathlib

English

For f : ι → α and a ∈ α, iSup f < a if and only if there exists b with b < a and f i ≤ b for all i.

Русский

Для функции f : ι → α и элемента a, iSup f < a тогда и только тогда, когда существует b < a такой, что f(i) ≤ b для всех i.

LaTeX

$$$\\\\forall {f : ι \\\\to α} {a : α}, \\\\left( iSup f < a \\\\right) \\\\Leftrightarrow \\\\exists b, b < a \\\\wedge \\\\forall i, f i \\\\le b$$$

Lean4

theorem iSup_lt_iff : iSup f < a ↔ ∃ b, b < a ∧ ∀ i, f i ≤ b :=
  ⟨fun h => ⟨iSup f, h, le_iSup f⟩, fun ⟨_, h, hb⟩ => (iSup_le hb).trans_lt h⟩

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