isGLB_lt_iff — Mathlib

English

Let a be the GLB of s in a linear order. Then a < b if and only if there exists c ∈ s with c < b.

Русский

Пусть a — наибольшая нижняя граница s в линейном порядке. Тогда a < b тогда и только тогда, когда существует c ∈ s такое, что c < b.

LaTeX

$$IsGLB s a → (a < b ↔ ∃ c ∈ s, c < b)$$

Lean4

theorem isGLB_lt_iff (h : IsGLB s a) : a < b ↔ ∃ c ∈ s, c < b :=
  lt_isLUB_iff h.dual

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