isCoatomic_iff — Mathlib

English

IsCoatomic is preserved by order isomorphisms: α coatomic iff β coatomic.

Русский

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

LaTeX

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

Lean4

protected theorem isCoatomic_iff [OrderTop α] [OrderTop β] (f : α ≃o β) : IsCoatomic α ↔ IsCoatomic β := by
  simp only [← isAtomic_dual_iff_isCoatomic, f.dual.isAtomic_iff]

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