l_sInf_u_image — Mathlib

English

If gi is a Galois insertion, then for any s ⊆ β, l(sInf(u''s)) = sInf s.

Русский

Пусть gi — связь Галуа; тогда для любого s ⊆ β выполняется l(infimum изображения u''s) = infimum s.

LaTeX

$$$$ l\left( \operatorname{sInf}(u''s) \right) = \operatorname{sInf}(s). $$$$

Lean4

theorem l_sInf_u_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) (s : Set β) :
    l (sInf (u '' s)) = sInf s := by rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]

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