isCoatom_of_l_top — Mathlib

English

For a GaloisCoinsertion with l top = top, if IsCoatom(l(a)) then IsCoatom(a).

Русский

Для GaloisCoinsertion с l top = top: IsCoatom(l(a)) ⇒ IsCoatom(a).

LaTeX

$$$\forall a,\ \text{IsCoatom}(l(a)) \Rightarrow \text{IsCoatom}(a)$$$

Lean4

theorem isCoatom_of_l_top [OrderTop α] [OrderTop β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u)
    (hbot : l ⊤ = ⊤) {a : α} (hb : IsCoatom (l a)) : IsCoatom a :=
  gi.dual.isAtom_of_u_bot hbot hb.dual

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