trivializationAt_proj_fst — Mathlib

English

The first component of the image under the trivialization at x.proj equals x.proj.

Русский

Первая компонента изображения тривиализации над x.proj равна x.proj.

LaTeX

$$$((\operatorname{trivializationAt}(F,E,x.proj)\,)(x)).\text{fst} = x.proj$$$

Lean4

theorem trivializationAt_proj_fst {x : TotalSpace F E} : ((trivializationAt F E x.proj) x).1 = x.proj :=
  Trivialization.coe_fst' _ <| mem_baseSet_trivializationAt F E x.proj

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