isGLB_u_image

Mathlib.Order.GaloisConnection.Basic

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

English

Dual to LUB preservation: the image under u preserves greatest lower bounds along sets.

Русский

Дуально к сохранению lub: образ через u сохраняет наибольшие нижние границы по множествам.

LaTeX

$$$$\\text{IsGLB}(u''s) (u b) \\text{ from IsGLB}(s,b)$$$$

Lean4

theorem isGLB_u_image {s : Set β} {b : β} (h : IsGLB s b) : IsGLB (u '' s) (u b) :=
  gc.dual.isLUB_l_image h

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

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

Разделы

Аффилиация

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