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

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.

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

ReflBEq α says that the BEq implementation is reflexive.

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

  Reflexivity for BEq.

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

EquivBEq says that the BEq implementation is an equivalence relation.

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

@[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 α] : EquivBEq α

Equations

• ⋯ = ⋯