isCoatomistic_iff — Mathlib

English

In a complete lattice that is coatomistic, every element b is the infimum of a set of coatoms.

Русский

В коатомистичной полной решетке каждый элемент является инфиминумом множества коатомов.

LaTeX

$$∃ s : Set α, b = sInf s ∧ ∀ a ∈ s, IsCoatom a$$

Lean4

nonrec theorem isCoatomistic_iff {α} [CompleteLattice α] :
    IsCoatomistic α ↔ ∀ b : α, ∃ s : Set α, b = sInf s ∧ ∀ a ∈ s, IsCoatom a := by
  simp_rw [isCoatomistic_iff, isGLB_iff_sInf_eq, eq_comm]

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