symmL_trivialization — Mathlib

English

The continuous linear equivalence at x for the trivialization is the identity equivalence.

Русский

Непрерывно-обозначенная эквивалентность линейности в точке x для тривиализации равна тождественной эквивалентности.

LaTeX

$$$$ (trivialization B F).continuousLinearEquivAt 𝕜 x (mem_univ _) = ContinuousLinearEquiv.refl 𝕜 F $$$$

Lean4

@[simp]
theorem symmL_trivialization (x : B) : (trivialization B F).symmL 𝕜 x = ContinuousLinearMap.id 𝕜 F := by ext;
  simp [trivialization_symm_apply B F]

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