setSymm — Mathlib

English

Define setSymm as the composition of the inverse and the coercion from the target of the pretrivialization.

Русский

Определим setSymm как композицию обратного и когерсии из множества-цели предтривиализации.

LaTeX

$$$\text{setSymm} = e.target.\text{restrict } e.toPartialEquiv.symm$$$

Lean4

/-- Composition of inverse and coercion from the subtype of the target. -/
def setSymm : e.target → Z :=
  e.target.restrict e.toPartialEquiv.symm

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