isCoatom_of_map_top_of_image — Mathlib

English

An order-embedding preserving top reflects coatoms: if f top = top and f(b) is a coatom, then b is a coatom.

Русский

Если отображение сохраняет верхнюю грань, то коатом сохраняется обратно: IsCoatom(f(b)) ⇒ IsCoatom(b).

LaTeX

$$$\forall b,\ \mathrm{IsCoatom}(f(b)) \Rightarrow \mathrm{IsCoatom}(b)$$$

Lean4

theorem isCoatom_of_map_top_of_image [OrderTop α] [OrderTop β] (f : β ↪o α) (htop : f ⊤ = ⊤) {b : β}
    (hb : IsCoatom (f b)) : IsCoatom b :=
  f.dual.isAtom_of_map_bot_of_image htop hb

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