Documentation

Init.Data.BEq

class PartialEquivBEq (α : Type u_1) [BEq α] :

PartialEquivBEq α says that the BEq implementation is a partial equivalence relation, that is:

  • it is symmetric: a == b → b == a
  • it is transitive: a == b → b == c → a == c.
  • symm : ∀ {a b : α}, (a == b) = true(b == a) = true

    Symmetry for BEq. If a == b then b == a.

  • trans : ∀ {a b c : α}, (a == b) = true(b == c) = true(a == c) = true

    Transitivity for BEq. If a == b and b == c then a == c.

Instances
    theorem PartialEquivBEq.symm {α : Type u_1} :
    ∀ {inst : BEq α} [self : PartialEquivBEq α] {a b : α}, (a == b) = true(b == a) = true

    Symmetry for BEq. If a == b then b == a.

    theorem PartialEquivBEq.trans {α : Type u_1} :
    ∀ {inst : BEq α} [self : PartialEquivBEq α] {a b c : α}, (a == b) = true(b == c) = true(a == c) = true

    Transitivity for BEq. If a == b and b == c then a == c.

    class ReflBEq (α : Type u_1) [BEq α] :

    ReflBEq α says that the BEq implementation is reflexive.

    • refl : ∀ {a : α}, (a == a) = true

      Reflexivity for BEq.

    Instances
      theorem ReflBEq.refl {α : Type u_1} :
      ∀ {inst : BEq α} [self : ReflBEq α] {a : α}, (a == a) = true

      Reflexivity for BEq.

      class EquivBEq (α : Type u_1) [BEq α] extends PartialEquivBEq , ReflBEq :

      EquivBEq says that the BEq implementation is an equivalence relation.

        Instances
          @[simp]
          theorem BEq.refl {α : Type u_1} [BEq α] [ReflBEq α] {a : α} :
          (a == a) = true
          theorem beq_of_eq {α : Type u_1} [BEq α] [ReflBEq α] {a : α} {b : α} :
          a = b(a == b) = true
          theorem BEq.symm {α : Type u_1} [BEq α] [PartialEquivBEq α] {a : α} {b : α} :
          (a == b) = true(b == a) = true
          theorem BEq.comm {α : Type u_1} [BEq α] [PartialEquivBEq α] {a : α} {b : α} :
          (a == b) = (b == a)
          theorem BEq.symm_false {α : Type u_1} [BEq α] [PartialEquivBEq α] {a : α} {b : α} :
          (a == b) = false(b == a) = false
          theorem BEq.trans {α : Type u_1} [BEq α] [PartialEquivBEq α] {a : α} {b : α} {c : α} :
          (a == b) = true(b == c) = true(a == c) = true
          theorem BEq.neq_of_neq_of_beq {α : Type u_1} [BEq α] [PartialEquivBEq α] {a : α} {b : α} {c : α} :
          (a == b) = false(b == c) = true(a == c) = false
          theorem BEq.neq_of_beq_of_neq {α : Type u_1} [BEq α] [PartialEquivBEq α] {a : α} {b : α} {c : α} :
          (a == b) = true(b == c) = false(a == c) = false
          @[instance 100]
          instance instEquivBEqOfLawfulBEq {α : Type u_1} [BEq α] [LawfulBEq α] :
          Equations
          • =