csSup_lt_iff — Mathlib

English

For a finite set s, sSup s < a if and only if every x ∈ s satisfies x < a.

Русский

Для конечного множества s, если sSup s < a тогда и только тогда, когда каждый x ∈ s удовлетворяет x < a.

LaTeX

$$$(hs : s.Finite) (h : s.Nonempty) : sSup s < a \Leftrightarrow \forall x ∈ s, x < a$$$

Lean4

theorem csSup_lt_iff (hs : s.Finite) (h : s.Nonempty) : sSup s < a ↔ ∀ x ∈ s, x < a :=
  ⟨fun h _ hx => (le_csSup hs.bddAbove hx).trans_lt h, fun H => H _ <| h.csSup_mem hs⟩

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