isAtom_iff — Mathlib

English

For an order isomorphism f, IsAtom(f(a)) ↔ IsAtom(a).

Русский

Для изоморфизма порядка f: IsAtom(f(a)) ↔ IsAtom(a).

LaTeX

$$$\forall a,\ \text{IsAtom}(f(a)) \iff \text{IsAtom}(a)$$$

Lean4

@[simp]
theorem isAtom_iff [OrderBot α] [OrderBot β] (f : α ≃o β) (a : α) : IsAtom (f a) ↔ IsAtom a :=
  ⟨f.toGaloisCoinsertion.isAtom_of_image, fun ha =>
    f.toGaloisInsertion.isAtom_of_u_bot (map_bot f.symm) <| (f.symm_apply_apply a).symm ▸ ha⟩

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