English
If f is monotone and there is a Galois connection above b between α and β, then the image filter map f applied to atTop on α equals atTop on β.
Русский
Если отображение f монотонно и между α и β существует галуа-соединение выше порога b, то образ фильтра map f на atTop(α) равен atTop(β).
LaTeX
$$$(\\forall c \\ge b)(\\exists x, f x = c \\land (\\forall a, f a \\le c \\iff a \\le x)) \\; \\Rightarrow \\; \\operatorname{map} f \\operatorname{atTop} = \\operatorname{atTop}$$$
Lean4
/-- A function `f` maps upwards closed sets (atTop sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connection above `b`. -/
theorem map_atTop_eq_of_gc_preorder [Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] [IsDirected β (· ≤ ·)] {f : α → β}
(hf : Monotone f) (b : β) (hgi : ∀ c ≥ b, ∃ x, f x = c ∧ ∀ a, f a ≤ c ↔ a ≤ x) : map f atTop = atTop :=
by
have : Nonempty α := (hgi b le_rfl).nonempty
choose! g hfg hgle using hgi
refine le_antisymm (hf.tendsto_atTop_atTop fun c ↦ ?_) ?_
· rcases exists_ge_ge c b with ⟨d, hcd, hbd⟩
exact ⟨g d, hcd.trans (hfg d hbd).ge⟩
· have : Nonempty α := ⟨g b⟩
rw [(atTop_basis.map f).ge_iff]
intro a _
filter_upwards [eventually_ge_atTop (f a), eventually_ge_atTop b] with c hac hbc
exact ⟨g c, (hgle _ hbc _).1 hac, hfg _ hbc⟩
