isGLB_upperBounds

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#isGLB_upperBounds

English

There is an equivalence: IsGLB(upperBounds(s), a) if and only if IsLUB(s, a).

Русский

Существуют эквивалентности: IsGLB(верхние границы s, a) эквивалентно IsLUB(s, a).

LaTeX

$$$IsGLB(upperBounds(s), a) \leftrightarrow IsLUB(s, a)$$$

Lean4

@[simp]
theorem isGLB_upperBounds : IsGLB (upperBounds s) a ↔ IsLUB s a :=
  @isLUB_lowerBounds αᵒᵈ _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru