English
A monotone f with a local Galois-connection above b induces equality map f atTop = atTop, provided certain gc conditions hold with a left adjoint g.
Русский
Монотонная функция f с локальной гало-связью над b порождает равенство map f atTop = atTop при выполнении соответствующих условий gc с левой переходной функцией g.
LaTeX
$$$\text{Если } f\text{ монотонна, и существует } g:\beta\to\alpha\text{ удовлетворяющее }\forall a,\forall c\ge b,\ f(a)\le c\iff a\le g(c)\ \text{и }\forall c\ge b,\ c\le f(g(c)),\\ тогда }\ \mathrm{map}\,f\ atTop = 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 α] [IsDirected α (· ≤ ·)] [PartialOrder β] [IsDirected β (· ≤ ·)] {f : α → β}
(g : β → α) (b : β) (hf : Monotone f) (gc : ∀ a, ∀ c ≥ b, f a ≤ c ↔ a ≤ g c) (hgi : ∀ c ≥ b, c ≤ f (g c)) :
map f atTop = atTop :=
map_atTop_eq_of_gc_preorder hf b fun c hc ↦ ⟨g c, le_antisymm ((gc _ _ hc).2 le_rfl) (hgi c hc), (gc · c hc)⟩
