u_iInf — Mathlib

English

Let α and β be complete lattices and l,u form a Galois connection. Then for any index set I and any f: I → β, u(inf_i f(i)) = inf_i u(f(i)). In words, the right adjoint u preserves arbitrary infima.

Русский

Пусть α и β — полные решетки и пары l, u образуют связь Галуа. Тогда для любого множества индексов I и функции f: I → β выполнено: u(inf_i f(i)) = inf_i u(f(i)). Другими словами, правое сопряжение сохраняет произвольный infimum.

LaTeX

$$$\\forall f,\\ u(\\inf_i f(i)) = \\inf_i u(f(i)).$$$

Lean4

theorem u_iInf {f : ι → β} : u (iInf f) = ⨅ i, u (f i) :=
  gc.dual.l_iSup

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