English
The fiberwise inverse to a trivialization e' is defined by composing the inverse of the pretrivialization with the fiber map, and outside the base set it is defined to be zero. Formally, for b ∈ B and y ∈ F, the value is e.toPretrivialization.symm b y (normalized by the zero outside the baseSet).
Русский
Функция, обратная по волокну к тривиализации e', задаётся через обратимую часть предварительной тривиализации и дополнительно обнуление за пределами базовой области.
LaTeX
$$$\\text{symm}_e(b,y) = e.toPretrivialization.symm\\; b\\; y$, и вне $e.baseSet$ принимает значение $0$$$
Lean4
/-- A fiberwise inverse to `e'`. The function `F → E x` that induces a local inverse
`B × F → TotalSpace F E` of `e'` on `e'.baseSet`. It is defined to be `0` outside `e'.baseSet`. -/
protected noncomputable def symm (e : Trivialization F (π F E)) (b : B) (y : F) : E b :=
e.toPretrivialization.symm b y
