u_sInf — Mathlib

English

Let α and β be complete lattices and l,u form a Galois connection. For any set s, u(sInf s) = ⨅ a∈s, u a. This is the dual statement to the one for sSup.

Русский

Пусть α и β — полные решетки и связь Галуа. Тогда для множества s выполняется: u(inf s) = inf_{a∈s} u(a).

LaTeX

$$$$ u\\big( \\inf s \\big) = \\inf_{a\\in s} u(a). $$$$

Lean4

theorem u_sInf {s : Set β} : u (sInf s) = ⨅ a ∈ s, u a :=
  gc.dual.l_sSup

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