lawful_beq_subsingleton — Mathlib

English

If α carries a LawfulBEq structure, then any two BEq α instances are equal; the BEq structure is unique.

Русский

Если у α имеется структура LawfulBEq, то любые две структуры BEq α равны; BEq-структура уникальна.

LaTeX

$$$ \forall inst1 inst2 : BEq \alpha, [LawfulBEq \alpha] \Rightarrow inst1 = inst2 $$$

Lean4

theorem lawful_beq_subsingleton {α : Type*} (inst1 : BEq α) (inst2 : BEq α) [@LawfulBEq α inst1] [@LawfulBEq α inst2] :
    inst1 = inst2 := by
  apply beq_ext
  intro x y
  classical simp only [beq_eq_decide]

Похожие утверждения