------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Lattice.Bundles using (DistributiveLattice)
module Algebra.Lattice.Properties.DistributiveLattice
{dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂)
where
import Algebra.Lattice.Properties.Lattice as LatticeProperties
open DistributiveLattice DL
open import Algebra.Definitions _≈_
open import Algebra.Lattice.Structures _≈_
open import Relation.Binary.Reasoning.Setoid setoid
------------------------------------------------------------------------
-- Export properties of lattices
open LatticeProperties lattice public
------------------------------------------------------------------------
-- The dual construction is also a distributive lattice.
∧-∨-isDistributiveLattice : IsDistributiveLattice _∧_ _∨_
∧-∨-isDistributiveLattice = record
{ isLattice = ∧-∨-isLattice
; ∨-distrib-∧ = ∧-distrib-∨
; ∧-distrib-∨ = ∨-distrib-∧
}
∧-∨-distributiveLattice : DistributiveLattice _ _
∧-∨-distributiveLattice = record
{ isDistributiveLattice = ∧-∨-isDistributiveLattice
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4