u_csInf

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

← MathLib Explorer

English

For gc, the dual statement to l_csSup' yields u( sInf s ) = sInf (u''s).

Русский

Для сопряжения Гали двойственная формулировка: u( inf s ) = inf( u''s ).

LaTeX

$$$ u(\mathrm{sInf} s) = \mathrm{sInf}(u''s) $$$

Lean4

theorem u_csInf (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) :
    u (sInf s) = ⨅ x : s, u x :=
  gc.dual.l_csSup hne hbdd

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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