map_cofinal — Mathlib

English

Let h be a Galois connection with maps f,g. If s is cofinal in α, then g '' s is cofinal in β.

Русский

Пусть h задаёт сопряжение Галуа с отображениями f,g. Если s софинально в α, то g''s софинально в β.

LaTeX

$$IsCofinal s → IsCofinal (g '' s)$$

Lean4

theorem map_cofinal [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) {s : Set α} (hs : IsCofinal s) :
    IsCofinal (g '' s) := by
  intro a
  obtain ⟨b, hb, hb'⟩ := hs (f a)
  exact ⟨g b, Set.mem_image_of_mem _ hb, h.le_iff_le.1 hb'⟩

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