mk — Mathlib · SciLib

English

Sym2.mk is the quotient map from α×α to Sym2 α.

Русский

Sym2.mk — это отображение-кпроксиматор из α×α в Sym2 α, т.е. квотент по отношению Rel α.

LaTeX

$$$$ \ Sym2.mk : \alpha \times \alpha \to Sym2\alpha \text{ is the quotient map}. $$$$

Lean4

/-- Constructor for `Sym2`. This is the quotient map `α × α → Sym2 α`. -/
protected abbrev mk {α : Type*} (p : α × α) : Sym2 α :=
  Quot.mk (Sym2.Rel α) p

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