equivQuotient — Mathlib

English

There is a natural equivalence between the index type ι and the quotient hs.Quotient, given by hs.equivQuotient.

Русский

Существует естественное биективное соответствие между индексным типом ι и квотиентом hs.Quotient, задаваемое hs.equivQuotient.

LaTeX

$$$ hs.equivQuotient : ι \simeq hs.Quotient $$$

Lean4

/-- The obvious equivalence between the quotient associated to an indexed partition and
the indexing type. -/
def equivQuotient : ι ≃ hs.Quotient :=
  (Setoid.quotientKerEquivOfRightInverse hs.index hs.some <| hs.index_some).symm

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