exists_lt_of_lt_csSup — Mathlib

English

In a linear order, if s is nonempty and b < sSup s, then there exists a ∈ s with b < a.

Русский

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

LaTeX

$$$ (s \neq \varnothing) \land (b < sSup s) \Rightarrow \exists a \in s, b < a $$$

Lean4

/-- When `b < sSup s`, there is an element `a` in `s` with `b < a`, if `s` is nonempty and the order
is a linear order. -/
theorem exists_lt_of_lt_csSup (hs : s.Nonempty) (hb : b < sSup s) : ∃ a ∈ s, b < a :=
  by
  contrapose! hb
  exact csSup_le hs hb

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