equivalence — Mathlib

English

The HasEquiv instance on Subtype p defines an equivalence relation on the subtype: the relation is reflexive, symmetric, and transitive.

Русский

Отношение эквивалентности на подтипе, задаваемое HasEquiv, является эквивалентностью: рефлексивность, симметричность и транзитивность.

LaTeX

$$$\text{Equivalence} \big(\text{Subtype}.\approx\_p\big)$$$

Lean4

theorem equivalence (p : α → Prop) : Equivalence (@HasEquiv.Equiv (Subtype p) _) :=
  .mk (Subtype.refl) (@Subtype.symm _ p _) (@Subtype.trans _ p _)

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