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