comap_embedding_atTop — Mathlib

English

If e is an order-embedding and every c in the codomain has a preimage below, then comap e atTop equals atTop.

Русский

Если e — вложение по порядку и для каждого c в кодомоде есть предобразец, меньший, то comap e atTop = atTop.

LaTeX

$$$\operatorname{comap} e \operatorname{atTop} = \operatorname{atTop}$$$

Lean4

theorem comap_embedding_atTop [Preorder β] [Preorder γ] {e : β → γ} (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂)
    (hu : ∀ c, ∃ b, c ≤ e b) : comap e atTop = atTop :=
  le_antisymm (le_iInf fun b => le_principal_iff.2 <| mem_comap.2 ⟨Ici (e b), mem_atTop _, fun _ => (hm _ _).1⟩)
    (tendsto_atTop_atTop_of_monotone (fun _ _ => (hm _ _).2) hu).le_comap

Похожие утверждения