lt_csSup_iff — Mathlib

English

In a densely ordered linear setting with a nonempty s bounded above, a < sSup s iff there exists b ∈ s with a < b.

Русский

В плотно упорядоченном линейном окружении с непустым s, ограниченным сверху, выполняется: a < sSup s тогда и только тогда, когда существует b ∈ s с a < b.

LaTeX

$$$ (BddAbove\ s) \land (s \neq \emptyset) \Rightarrow (a < sSup s \iff \exists b \in s, a < b)$$$

Lean4

theorem lt_csSup_iff (hb : BddAbove s) (hs : s.Nonempty) : a < sSup s ↔ ∃ b ∈ s, a < b :=
  lt_isLUB_iff <| isLUB_csSup hs hb

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