English
Let gi be a Galois insertion and s ⊆ β with hs: IsGLB (u''s) a. Then IsGLB s (l a).
Русский
Пусть gi — связь Галуа; если s ⊆ β и hs: IsGLB(u''s) a, тогда IsGLB s (l a).
LaTeX
$$$$ \operatorname{IsGLB}(u''s, a) \Rightarrow \operatorname{IsGLB}(s, l(a)). $$$$
Lean4
theorem isGLB_of_u_image [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α}
(hs : IsGLB (u '' s) a) : IsGLB s (l a) :=
⟨fun _ hx => gi.gc.l_le <| hs.1 <| mem_image_of_mem _ hx, fun x hx =>
(gi.le_l_u x).trans <| gi.gc.monotone_l <| hs.2 <| gi.gc.monotone_u.mem_lowerBounds_image hx⟩