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.

theorem PartialEquivBEq.symm {α : Type u_1} [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} [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 α] : Prop

ReflBEq α says that the BEq implementation is reflexive.

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

  Reflexivity for BEq.

theorem ReflBEq.refl {α : Type u_1} [BEq α] [self : ReflBEq α] {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.

@[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

• ⋯ = ⋯