English
If there exists a left adjoint g and gc-type relations above b between f and g, then map f atTop equals atTop.
Русский
Если существует левая сопряженная g и gc-подобные условия между f и g над b, то map f atTop = atTop.
LaTeX
$$$\exists g:\beta\to\alpha,\ b:\beta,\ hf:\mathrm{Monotone}(f),\ gc:\forall a,\forall c\ge b,\ f(a)\le c \iff a\le g(c),\ hgi:\forall c\ge b,\ c\le f(g(c)) \Rightarrow \mathrm{map}\ f\ atTop = atTop$$$
Lean4
/-- The `atTop` filter for an open interval `Ici a` comes from the `atTop` filter in the ambient
order. -/
theorem atTop_Ici_eq [Preorder α] [IsDirected α (· ≤ ·)] (a : α) : atTop = comap ((↑) : Ici a → α) atTop := by
rw [← map_val_Ici_atTop a, comap_map Subtype.coe_injective]
