eq_equivalence — Mathlib

English

Equality is an equivalence relation: reflexive, symmetric, and transitive.

Русский

Равенство является эквивалентным отношением: рефлексивно, симметрично и транзитивно.

LaTeX

$$$(\\forall x\\in\\alpha, x=x) \\land (\\forall x,y\\in\\alpha, x=y \\rightarrow y=x) \\land (\\forall x,y,z\\in\\alpha, x=y \\rightarrow y=z \\rightarrow x=z)$$$

Lean4

theorem eq_equivalence {α : Sort*} : Equivalence (@Eq α) :=
  ⟨Eq.refl, @Eq.symm _, @Eq.trans _⟩
    -- These were migrated to Batteries but the `@[simp]` attributes were (mysteriously?) removed.

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