English
Dual of the previous result: under a monotone map with a Galois connection above b in the dual order, the image of atBot equals atBot.
Русский
Дуальная версия предыдущего утверждения: при монотонном отображении с галуа-соединением выше b в двойном порядке образ atBot равен atBot.
LaTeX
$$$(\\forall c \\ge b)(\\exists x, f x = c \\land (\\forall a, f a \\le c \\iff a \\le x)) \\Rightarrow \\map f \\operatorname{atBot} = \\operatorname{atBot}$$$
Lean4
theorem map_atBot_eq_of_gc [Preorder α] [IsDirected α (· ≥ ·)] [PartialOrder β] [IsDirected β (· ≥ ·)] {f : α → β}
(g : β → α) (b' : β) (hf : Monotone f) (gc : ∀ a, ∀ b ≤ b', b ≤ f a ↔ g b ≤ a) (hgi : ∀ b ≤ b', f (g b) ≤ b) :
map f atBot = atBot :=
map_atTop_eq_of_gc (α := αᵒᵈ) (β := βᵒᵈ) _ _ hf.dual gc hgi
