lt_isGLB_iff — Mathlib

English

If a is the GLB of s, then b < a iff there exists c ∈ lowerBounds(s) with b < c.

Русский

Если a — ГЛБ множества s, то b < a тогда и только тогда, когда существует c ∈ нижних границ s such that b < c.

LaTeX

$$$IsGLB s a \rightarrow (b < a \\Leftrightarrow \\exists c \\in \lowerBounds(s), b < c)$$$

Lean4

theorem lt_isGLB_iff (ha : IsGLB s a) : b < a ↔ ∃ c ∈ lowerBounds s, b < c :=
  isLUB_lt_iff ha.dual

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