isGLB_congr — Mathlib

English

If two sets have the same lower bounds, then being a greatest lower bound is equivalent for the two sets.

Русский

Если два множества имеют одинаковые нижние границы, то быть наибольшей нижней границей для них эквивалентно.

LaTeX

$$$$ \operatorname{lowerBounds}(s) = \operatorname{lowerBounds}(t) \Rightarrow (\mathrm{IsGLB}(s,a) \iff \mathrm{IsGLB}(t,a)). $$$$

Lean4

theorem isGLB_congr (h : lowerBounds s = lowerBounds t) : IsGLB s a ↔ IsGLB t a := by rw [IsGLB, IsGLB, h]

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