toCompleteDistribLattice — Mathlib

English

A finite bounded distributive lattice is completely distributive.

Русский

Конечная ограниченная дискретная решётка полностью распределима.

LaTeX

$$[DistribLattice α] [BoundedOrder α] ⇒ CompleteDistribLattice α$$

Lean4

/-- A finite bounded distributive lattice is completely distributive. -/
noncomputable abbrev toCompleteDistribLattice [DistribLattice α] [BoundedOrder α] : CompleteDistribLattice α :=
  .ofMinimalAxioms
    (toCompleteDistribLatticeMinimalAxioms _)
      -- See note [reducible non-instances]

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