isCoatomic — Mathlib

English

If every π(i) is top-anchored and coatomic, then the product ∀ i, π(i) is coatomic.

Русский

Если каждый π(i) имеет верхний элемент и коатомарность, то произведение ∀ i, π(i) коатомарно.

LaTeX

$$$ IsCoatomic\left(\forall i,\ π(i)\right) $$$

Lean4

instance isCoatomic [∀ i, PartialOrder (π i)] [∀ i, OrderTop (π i)] [∀ i, IsCoatomic (π i)] : IsCoatomic (∀ i, π i) :=
  isAtomic_dual_iff_isCoatomic.1 <| show IsAtomic (∀ i, (π i)ᵒᵈ) from inferInstance

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