continuousLinearEquivAt_trivialization

English

The continuous-linear equivalence at x for the trivialization coincides with the identity equivalence.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem continuousLinearEquivAt_trivialization (x : B) :
    (trivialization B F).continuousLinearEquivAt 𝕜 x (mem_univ _) = ContinuousLinearEquiv.refl 𝕜 F := by ext; simp

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