isAtom_iff — Mathlib

English

Under an isomorphism of bounded orders, IsAtomic is preserved both ways.

Русский

При отображении между ограниченными порядками атомность сохраняется в обе стороны.

LaTeX

$$$\forall f,\text{OrderIso}(\alpha,\beta) \Rightarrow (\mathrm{IsAtomic}(\alpha) \iff \mathrm{IsAtomic}(\beta))$$$

Lean4

theorem isAtom_iff [OrderBot α] [OrderBot β] [IsAtomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u)
    (h_atom : ∀ b, IsAtom b → l (u b) = b) (a : α) : IsAtom (l a) ↔ IsAtom a :=
  gi.dual.isCoatom_iff h_atom a

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