trivialization_symm_apply — Mathlib

English

Symmetry of the trivialization acts as the identity on the fiber component for zero fiber.

Русский

Симметрия тривиализации действует как тождество на волокне при нулевом волокне.

LaTeX

$$$ \text{Trivialization}.symm\_toFun' (b,f) = f \quad (\text{for } f = 0 \text{ if } F \text{ has } 0)$$$

Lean4

@[simp]
theorem trivialization_symm_apply [Zero F] (b : B) (f : F) : (trivialization B F).symm b f = f := by
  simp [trivialization, homeomorphProd, TotalSpace.toProd, Trivialization.symm, Pretrivialization.symm,
    Trivialization.toPretrivialization]

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