isStronglyCoatomic — Mathlib

English

Let α be a lattice with a top element that is lower-modular and coatomistic. Then α is strongly coatomic.

Русский

Пусть α — решетка с максимумом, являющаяся нижнемодульной и коатомной. Тогда α сильно коатомна.

LaTeX

$$$ (OrderTop\ α) \land (IsLowerModularLattice\ α) \land (IsCoatomistic\ α) \Rightarrow IsStronglyCoatomic\ α $$$

Lean4

/-- A lower-modular lattice that is coatomistic is strongly coatomic.
Not an instance to prevent loops. -/
theorem isStronglyCoatomic [OrderTop α] [IsLowerModularLattice α] [IsCoatomistic α] : IsStronglyCoatomic α :=
  by
  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]
  exact Lattice.isStronglyAtomic

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