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 Std.Internal.Do.CompleteLattice.instReflRel_std {l : Sort u_1} [Lean.Order.CompleteLattice l] : Refl fun (x1 x2 : l) => Lean.Order.PartialOrder.rel x1 x2

@[instance_reducible]

instance Std.Internal.Do.CompleteLattice.instTransRel_std {l : Sort u_1} [Lean.Order.CompleteLattice l] : Trans (fun (x1 x2 : l) => Lean.Order.PartialOrder.rel x1 x2) (fun (x1 x2 : l) => Lean.Order.PartialOrder.rel x1 x2) fun (x1 x2 : l) => Lean.Order.PartialOrder.rel x1 x2

Equations

• Std.Internal.Do.CompleteLattice.instTransRel_std = { trans := ⋯ }

instance Std.Internal.Do.CompleteLattice.instAntisymmRel_std {l : Sort u_1} [Lean.Order.CompleteLattice l] : Antisymm fun (x1 x2 : l) => Lean.Order.PartialOrder.rel x1 x2

instance Std.Internal.Do.CompleteLattice.instCommutativeMeet {l : Type u_1} [Lean.Order.CompleteLattice l] : Commutative fun (x1 x2 : l) => Lean.Order.meet x1 x2

instance Std.Internal.Do.CompleteLattice.instCommutativeJoin {l : Type u_1} [Lean.Order.CompleteLattice l] : Commutative fun (x1 x2 : l) => Lean.Order.join x1 x2

instance Std.Internal.Do.CompleteLattice.instAssociativeMeet {l : Type u_1} [Lean.Order.CompleteLattice l] : Associative fun (x1 x2 : l) => Lean.Order.meet x1 x2

instance Std.Internal.Do.CompleteLattice.instAssociativeJoin {l : Type u_1} [Lean.Order.CompleteLattice l] : Associative fun (x1 x2 : l) => Lean.Order.join x1 x2

instance Std.Internal.Do.CompleteLattice.instIdempotentOpMeet {l : Type u_1} [Lean.Order.CompleteLattice l] : IdempotentOp fun (x1 x2 : l) => Lean.Order.meet x1 x2

instance Std.Internal.Do.CompleteLattice.instIdempotentOpJoin {l : Type u_1} [Lean.Order.CompleteLattice l] : IdempotentOp fun (x1 x2 : l) => Lean.Order.join x1 x2

instance Std.Internal.Do.CompleteLattice.instLeftIdentityMeetTop {l : Type u_1} [Lean.Order.CompleteLattice l] : LeftIdentity (fun (x1 x2 : l) => Lean.Order.meet x1 x2) Lean.Order.top

instance Std.Internal.Do.CompleteLattice.instRightIdentityMeetTop {l : Type u_1} [Lean.Order.CompleteLattice l] : RightIdentity (fun (x1 x2 : l) => Lean.Order.meet x1 x2) Lean.Order.top

instance Std.Internal.Do.CompleteLattice.instLeftIdentityJoinBot {l : Type u_1} [Lean.Order.CompleteLattice l] : LeftIdentity (fun (x1 x2 : l) => Lean.Order.join x1 x2) Lean.Order.bot

instance Std.Internal.Do.CompleteLattice.instRightIdentityJoinBot {l : Type u_1} [Lean.Order.CompleteLattice l] : RightIdentity (fun (x1 x2 : l) => Lean.Order.join x1 x2) Lean.Order.bot

instance Std.Internal.Do.CompleteLattice.instLawfulIdentityMeetTop {l : Type u_1} [Lean.Order.CompleteLattice l] : LawfulIdentity (fun (x1 x2 : l) => Lean.Order.meet x1 x2) Lean.Order.top

instance Std.Internal.Do.CompleteLattice.instLawfulIdentityJoinBot {l : Type u_1} [Lean.Order.CompleteLattice l] : LawfulIdentity (fun (x1 x2 : l) => Lean.Order.join x1 x2) Lean.Order.bot