isLUB_of_l_image — Mathlib

English

If gi is a Galois Coinsertion and IsLUB of l''s image equals a, then IsLUB of s with u(a).

Русский

Если gi — связь Галуа-коинсерция и IsLUB(l''s image) a, то IsLUB s (u a).

LaTeX

$$$$ \operatorname{IsLUB}\big(\{l(s) : s\in S\}, a\big) \Rightarrow \operatorname{IsLUB}(S, u(a)). $$$$

Lean4

theorem isLUB_of_l_image [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set α} {a : β}
    (hs : IsLUB (l '' s) a) : IsLUB s (u a) :=
  gi.dual.isGLB_of_u_image hs

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