isLUB_of_u_image — Mathlib

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⟩

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