De Morgan and Kleene algebras: instances

OrderDual, Prod, and Pi instances for LatticeWithInvolution, DeMorganAlgebra, and Order.KleeneAlgebra, plus the involution bundled as an order isomorphism α ≃o αᵒᵈ — the Defs/Basic split mathlib uses for BooleanAlgebra (cf. OrderIso.compl there, which this generalizes past complementation).

OrderDual

@[instance_reducible]

instance instLatticeWithInvolutionOrderDual {α : Type u_1} [LatticeWithInvolution α] : LatticeWithInvolution αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instDeMorganAlgebraOrderDual {α : Type u_1} [DeMorganAlgebra α] : DeMorganAlgebra αᵒᵈ

Equations

• instDeMorganAlgebraOrderDual = { toDistribLattice := inferInstance, toBoundedOrder := inferInstance.toBoundedOrder, toCompl := inferInstance.toCompl, compl_compl := ⋯, compl_le_compl := ⋯ }

@[instance_reducible]

instance instKleeneAlgebraOrderDual {α : Type u_1} [Order.KleeneAlgebra α] : Order.KleeneAlgebra αᵒᵈ

Equations

• instKleeneAlgebraOrderDual = { toDeMorganAlgebra := instDeMorganAlgebraOrderDual, inf_compl_le_sup_compl := ⋯ }

Prod

@[instance_reducible]

instance instLatticeWithInvolutionProd {α : Type u_1} {β : Type u_2} [LatticeWithInvolution α] [LatticeWithInvolution β] : LatticeWithInvolution (α × β)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instDeMorganAlgebraProd {α : Type u_1} {β : Type u_2} [DeMorganAlgebra α] [DeMorganAlgebra β] : DeMorganAlgebra (α × β)

Equations

• instDeMorganAlgebraProd = { toDistribLattice := inferInstance, toBoundedOrder := inferInstance.toBoundedOrder, toCompl := inferInstance.toCompl, compl_compl := ⋯, compl_le_compl := ⋯ }

@[instance_reducible]

instance instKleeneAlgebraProd {α : Type u_1} {β : Type u_2} [Order.KleeneAlgebra α] [Order.KleeneAlgebra β] : Order.KleeneAlgebra (α × β)

Equations

• instKleeneAlgebraProd = { toDeMorganAlgebra := instDeMorganAlgebraProd, inf_compl_le_sup_compl := ⋯ }

Pi

@[instance_reducible]

instance instLatticeWithInvolutionForall {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → LatticeWithInvolution (π i)] : LatticeWithInvolution ((i : ι) → π i)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instDeMorganAlgebraForall {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → DeMorganAlgebra (π i)] : DeMorganAlgebra ((i : ι) → π i)

Equations

• instDeMorganAlgebraForall = { toDistribLattice := inferInstance, toBoundedOrder := inferInstance.toBoundedOrder, toCompl := inferInstance.toCompl, compl_compl := ⋯, compl_le_compl := ⋯ }

@[instance_reducible]

instance instKleeneAlgebraForall {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → Order.KleeneAlgebra (π i)] : Order.KleeneAlgebra ((i : ι) → π i)

Equations

• instKleeneAlgebraForall = { toDeMorganAlgebra := instDeMorganAlgebraForall, inf_compl_le_sup_compl := ⋯ }

The involution as an order isomorphism

def LatticeWithInvolution.complOrderIso (α : Type u_3) [LatticeWithInvolution α] : α ≃o αᵒᵈ

The involution bundled as an order isomorphism onto the order dual — the generalization of mathlib's OrderIso.compl from BooleanAlgebra to any LatticeWithInvolution.

Equations

• LatticeWithInvolution.complOrderIso α = { toFun := fun (a : α) => OrderDual.toDual aᶜ, invFun := fun (a : αᵒᵈ) => (OrderDual.ofDual a)ᶜ, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }