linearMapAt_trivialization — Mathlib

English

For the trivialization of a bundle, the linear map at any point x equals the identity map on the fiber.

Русский

Для тривиализации связки линейный переход в точке x равен тождественному отображению на волокне.

LaTeX

$$$$ (trivialization B F).linearMapAt 𝕜 x = LinearMap.id $$$$

Lean4

@[simp]
theorem linearMapAt_trivialization (x : B) : (trivialization B F).linearMapAt 𝕜 x = LinearMap.id :=
  by
  ext v
  rw [Trivialization.coe_linearMapAt_of_mem _ (by simp)]
  rfl

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