symm_proj_apply — Mathlib

English

For a trivialization e, and a base point z with hz ∈ e.baseSet, applying the inverse to z yields a point whose base projection equals z.proj and whose fiber component is inverse-projected accordingly.

Русский

Для тривиализации e и z с hz ∈ e.baseSet, применение обратной карты к z дает точку с базовой проекцией z.proj и корректной фиберной компонентой.

LaTeX

$$$e.symm z.proj (e z).2 = z.2$$$

Lean4

theorem symm_proj_apply (e : Trivialization F (π F E)) (z : TotalSpace F E) (hz : z.proj ∈ e.baseSet) :
    e.symm z.proj (e z).2 = z.2 :=
  e.toPretrivialization.symm_proj_apply z hz

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