instCoeSortType — Mathlib

English

DiscreteQuotient X can be treated as a type whose elements are equivalence classes of X under ∼.

Русский

Факторпространство X/~ можно рассматривать как тип, состоящий из классов эквивалентности элементов X по отношению ≈.

LaTeX

$$$ X/\\sim \\;\\text{is a type of equivalence classes on }X$$$

Lean4

instance : CoeSort (DiscreteQuotient X) (Type _) :=
  ⟨fun S => Quotient S.toSetoid⟩

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