ofMinimalAxioms

Mathlib.Order.CompleteBooleanAlgebra

URI: https://scilib.ai/kg/mathlib#CompletelyDistribLattice.ofMinimalAxioms

Lean4

/-- Construct a completely distributive lattice instance using the minimal amount of work needed.

This sets `a ⇨ b := sSup {c | c ⊓ a ≤ b}`, `aᶜ := a ⇨ ⊥`, `a \ b := sInf {c | a ≤ b ⊔ c}` and
`￢a := ⊤ \ a`. -/
-- See note [reducible non-instances]

abbrev ofMinimalAxioms (minAx : MinimalAxioms α) : CompletelyDistribLattice α
    where
  __ := minAx
  __ := CompleteDistribLattice.ofMinimalAxioms minAx.toCompleteDistribLattice

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru