English
If Ici a is contained in a subset s of α, then the inclusion map from s into α takes the atTop filter to atTop.
Русский
Если множество ICI a содержится в s ⊆ α, то включение s → α переносит фильтр atTop в atTop.
LaTeX
$$$\forall a,\; (\text{Ici } a\subseteq s)\Rightarrow \mathrm{map}\left(\iota:\, s\to \alpha\right)\mathrm{atTop} = \mathrm{atTop}$$$
Lean4
theorem map_val_atTop_of_Ici_subset [Preorder α] [IsDirected α (· ≤ ·)] {a : α} {s : Set α} (h : Ici a ⊆ s) :
map ((↑) : s → α) atTop = atTop :=
by
choose f hl hr using exists_ge_ge (α := α)
have : DirectedOn (· ≤ ·) s := fun x _ y _ ↦
⟨f a (f x y), h <| hl _ _, (hl x y).trans (hr _ _), (hr x y).trans (hr _ _)⟩
have : IsDirected s (· ≤ ·) := by
rw [directedOn_iff_directed] at this
rwa [← directed_id_iff]
refine map_atTop_eq_of_gc_preorder (Subtype.mono_coe _) a fun c hc ↦ ?_
exact ⟨⟨c, h hc⟩, rfl, fun _ ↦ .rfl⟩
