isCoatom_iff — Mathlib

English

Under a GaloisInsertion with appropriate top/bottom conditions, IsCoatom(l(a)) ↔ IsCoatom(a).

Русский

При соблюдении условий верхнего/нижнего пределов, IsCoatom(l(a)) ↔ IsCoatom(a).

LaTeX

$$$\forall a,\ \mathrm{IsCoatom}(\,l(a)\,) \iff \mathrm{IsCoatom}(a)$$$

Lean4

theorem isCoatom_iff [OrderTop α] [OrderTop β] [IsCoatomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u)
    (htop : l ⊤ = ⊤) (h_coatom : ∀ b, IsCoatom b → l (u b) = b) (b : β) : IsCoatom (u b) ↔ IsCoatom b :=
  gi.dual.isAtom_iff htop h_coatom b

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