isCoatom_iff' — Mathlib

English

A variant: under additional 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) (a : α) : IsCoatom (l a) ↔ IsCoatom a :=
  gi.dual.isAtom_iff' htop h_coatom a

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