symmₗ_trivialization — Mathlib

English

The left-linear part of the trivialization’s symmetry is the identity linear map on each fiber.

Русский

Левая линейная часть симметрии тривиализации равна тождественному линейному отображению на каждом волокне.

LaTeX

$$$$ (trivialization B F).symmL 𝕜 x = ContinuousLinearMap.id 𝕜 F $$$$

Lean4

@[simp]
theorem symmₗ_trivialization (x : B) : (trivialization B F).symmₗ 𝕜 x = LinearMap.id := by ext;
  simp [Trivialization.coe_symmₗ, trivialization_symm_apply B F]

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