Algebraic typeclass instances for CompleteLattice #
The order ⊑ is reflexive, transitive and antisymmetric, and meet and join are commutative,
associative and idempotent monoid operations with units ⊤ and ⊥. These instances expose that
structure to the generic algebra in Std (Std.Commutative, Std.Associative, Trans, ...).
instance
Lean.Order.instReflRel_std
{l : Sort u_1}
[CompleteLattice l]
:
Std.Refl fun (x1 x2 : l) => PartialOrder.rel x1 x2
@[instance_reducible]
instance
Lean.Order.instTransRel_std
{l : Sort u_1}
[CompleteLattice l]
:
Trans (fun (x1 x2 : l) => PartialOrder.rel x1 x2) (fun (x1 x2 : l) => PartialOrder.rel x1 x2) fun (x1 x2 : l) =>
PartialOrder.rel x1 x2
Equations
- Lean.Order.instTransRel_std = { trans := ⋯ }
instance
Lean.Order.instAntisymmRel_std
{l : Sort u_1}
[CompleteLattice l]
:
Std.Antisymm fun (x1 x2 : l) => PartialOrder.rel x1 x2
instance
Lean.Order.instCommutativeMeet
{l : Type u_1}
[CompleteLattice l]
:
Std.Commutative fun (x1 x2 : l) => meet x1 x2
instance
Lean.Order.instCommutativeJoin
{l : Type u_1}
[CompleteLattice l]
:
Std.Commutative fun (x1 x2 : l) => join x1 x2
instance
Lean.Order.instAssociativeMeet
{l : Type u_1}
[CompleteLattice l]
:
Std.Associative fun (x1 x2 : l) => meet x1 x2
instance
Lean.Order.instAssociativeJoin
{l : Type u_1}
[CompleteLattice l]
:
Std.Associative fun (x1 x2 : l) => join x1 x2
instance
Lean.Order.instIdempotentOpMeet
{l : Type u_1}
[CompleteLattice l]
:
Std.IdempotentOp fun (x1 x2 : l) => meet x1 x2
instance
Lean.Order.instIdempotentOpJoin
{l : Type u_1}
[CompleteLattice l]
:
Std.IdempotentOp fun (x1 x2 : l) => join x1 x2
instance
Lean.Order.instLawfulCommIdentityMeetTop
{l : Type u_1}
[CompleteLattice l]
:
Std.LawfulCommIdentity (fun (x1 x2 : l) => meet x1 x2) top
instance
Lean.Order.instLawfulCommIdentityJoinBot
{l : Type u_1}
[CompleteLattice l]
:
Std.LawfulCommIdentity (fun (x1 x2 : l) => join x1 x2) bot