isAtomic_iff — Mathlib

English

Under an order isomorphism, IsAtomic is preserved: α is atomic iff β is atomic.

Русский

При изоморфизме порядка атомность сохраняется: α атомарен тогда и только тогда β атомарен.

LaTeX

$$$\forall f:\alpha \simeq_o \beta,\ \text{IsAtomic}(\alpha) \iff \text{IsAtomic}(\beta)$$$

Lean4

protected theorem isAtomic_iff [OrderBot α] [OrderBot β] (f : α ≃o β) : IsAtomic α ↔ IsAtomic β := by
  simp only [isAtomic_iff, f.surjective.forall, f.surjective.exists, ← map_bot f, f.eq_iff_eq, f.le_iff_le,
    f.isAtom_iff]

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