isGLB_of_u_image — Mathlib

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⟩

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