le_isGLB_iff — Mathlib

English

If s has a greatest lower bound a, then b ≤ a iff b is a lower bound of s.

Русский

Если множество s имеет наибольшую нижнюю грань a, то для любого b верно: b ≤ a тогда и только если b является нижней границей s.

LaTeX

$$$IsGLB(s,a) \\rightarrow (b \\le a \\iff b \\in \\mathrm{lowerBounds}(s))$$$

Lean4

theorem le_isGLB_iff (h : IsGLB s a) : b ≤ a ↔ b ∈ lowerBounds s :=
  by
  rw [h.lowerBounds_eq]
  rfl

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