isLUB_congr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isLUB_congr (h : upperBounds s = upperBounds t) : IsLUB s a ↔ IsLUB t a := by rw [IsLUB, IsLUB, h]

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