isLUB_u

Mathlib.Order.GaloisConnection.Basic

URI: https://scilib.ai/kg/mathlib#GaloisConnection.isLUB_u

English

If s ⊆ β has lub b, then u maps s to a set with lub u b, i.e., lub preserved under u.

Русский

Если s ⊆ β имеет верхнюю границу b, то образ через u множества s имеет верхнюю границу u b; то есть lub сохраняется через u.

LaTeX

$$$$ IsLUB\\{a : α \\mid a \\le l a' \\} (u b) $$$$

Lean4

theorem isLUB_u {b : β} : IsLUB {a | l a ≤ b} (u b) :=
  gc.isGreatest_u.isLUB

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

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

Разделы

Аффилиация

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