symm — Mathlib

English

If the base set does not contain b, then the symmetry map sends b to the zero element in the fiber E b.

Русский

Если b не принадлежит базовому множеству, симметрическое отображение отправляет b в ноль в волокне E b.

LaTeX

$$$\text{If } b\notin e.baseSet:\ e.symm\,b\,y=0$$$

Lean4

/-- A fiberwise inverse to `e`. This is the function `F → E b` 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 : Pretrivialization F (π F E)) (b : B) (y : F) : E b :=
  if hb : b ∈ e.baseSet then cast (congr_arg E (e.proj_symm_apply' hb)) (e.toPartialEquiv.symm (b, y)).2 else 0

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