comap_embedding_atBot — Mathlib

English

Dual to comap atTop: if e is an order-embedding and every c has a preimage, then comap e atBot equals atBot.

Русский

Дуальная версия: если e — вложение, то comap e atBot = atBot.

LaTeX

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

Lean4

theorem comap_embedding_atBot [Preorder β] [Preorder γ] {e : β → γ} (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂)
    (hu : ∀ c, ∃ b, e b ≤ c) : comap e atBot = atBot :=
  @comap_embedding_atTop βᵒᵈ γᵒᵈ _ _ e (Function.swap hm) hu

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