English
Let gi be a Galois insertion between preorders; if IsLUB of l''s image equals a, then IsLUB of s with u(a).
Русский
Пусть gi — связь Галуа между предотношениями; если IsLUB изображения l''s равен a, то IsLUB множества s с элементом u(a).
LaTeX
$$$$ \operatorname{IsLUB}(l''s, a) \Rightarrow \operatorname{IsLUB}(s, l(a)). $$$$
Lean4
theorem isLUB_of_u_image [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α}
(hs : IsLUB (u '' s) a) : IsLUB s (l a) :=
⟨fun x hx => (gi.le_l_u x).trans <| gi.gc.monotone_l <| hs.1 <| mem_image_of_mem _ hx, fun _ hx =>
gi.gc.l_le <| hs.2 <| gi.gc.monotone_u.mem_upperBounds_image hx⟩