HepLean Documentation

Mathlib.Logic.OpClass

Typeclasses for commuting heterogeneous operations #

The three classes in this file are for two-argument functions where one input is of type α, the output is of type β and the other input is of type α or β. They express the property that permuting arguments of type α does not change the result.

Main definitions #

source
class IsSymmOp {α : Sort u} {β : Sort v} (op : α → α → β) :
Prop

IsSymmOp op where op : α → α → β says that op is a symmetric operation, i.e. op a b = op b a. It is the natural generalisation of Std.Commutative (β = α) and IsSymm (β = Prop).

  • symm_op : ∀ (a b : α), op a b = op b a

    A symmetric operation satisfies op a b = op b a.

Instances
    source
    theorem IsSymmOp.symm_op {α : Sort u} {β : Sort v} {op : α → α → β} [self : IsSymmOp op] (a : α) (b : α) :
    op a b = op b a

    A symmetric operation satisfies op a b = op b a.

    source
    class LeftCommutative {α : Sort u} {β : Sort v} (op : α → β → β) :
    Prop

    LeftCommutative op where op : α → β → β says that op is a left-commutative operation, i.e. op a₁ (op a₂ b) = op a₂ (op a₁ b).

    • left_comm : ∀ (a₁ a₂ : α) (b : β), op a₁ (op a₂ b) = op a₂ (op a₁ b)

      A left-commutative operation satisfies op a₁ (op a₂ b) = op a₂ (op a₁ b).

    Instances
      source
      theorem LeftCommutative.left_comm {α : Sort u} {β : Sort v} {op : α → β → β} [self : LeftCommutative op] (a₁ : α) (a₂ : α) (b : β) :
      op a₁ (op a₂ b) = op a₂ (op a₁ b)

      A left-commutative operation satisfies op a₁ (op a₂ b) = op a₂ (op a₁ b).

      source
      class RightCommutative {α : Sort u} {β : Sort v} (op : β → α → β) :
      Prop

      RightCommutative op where op : β → α → β says that op is a right-commutative operation, i.e. op (op b a₁) a₂ = op (op b a₂) a₁.

      • right_comm : ∀ (b : β) (a₁ a₂ : α), op (op b a₁) a₂ = op (op b a₂) a₁

        A right-commutative operation satisfies op (op b a₁) a₂ = op (op b a₂) a₁.

      Instances
        source
        theorem RightCommutative.right_comm {α : Sort u} {β : Sort v} {op : β → α → β} [self : RightCommutative op] (b : β) (a₁ : α) (a₂ : α) :
        op (op b a₁) a₂ = op (op b a₂) a₁

        A right-commutative operation satisfies op (op b a₁) a₂ = op (op b a₂) a₁.

        source
        @[instance 100]
        instance isSymmOp_of_isCommutative (α : Sort u) (op : α → α → α) [Std.Commutative op] :
        IsSymmOp op
        Equations
        • ⋯ = ⋯
        source
        theorem IsSymmOp.flip_eq {α : Sort u} {β : Sort v} (op : α → α → β) [IsSymmOp op] :
        flip op = op
        source
        instance instRightCommutativeOfLeftCommutative {α : Sort u} {β : Sort v} {f : α → β → β} [h : LeftCommutative f] :
        RightCommutative fun (x : β) (y : α) => f y x
        Equations
        • ⋯ = ⋯
        source
        instance instLeftCommutativeOfRightCommutative {α : Sort u} {β : Sort v} {f : β → α → β} [h : RightCommutative f] :
        LeftCommutative fun (x : α) (y : β) => f y x
        Equations
        • ⋯ = ⋯
        source
        instance instLeftCommutativeOfCommutativeOfAssociative {α : Sort u} {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] :
        LeftCommutative f
        Equations
        • ⋯ = ⋯
        source
        instance instRightCommutativeOfCommutativeOfAssociative {α : Sort u} {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] :
        RightCommutative f
        Equations
        • ⋯ = ⋯