lift — Mathlib

English

The local lifting through a Trivialization T sends a point z ∈ Z and a base point b ∈ B to the unique z' ∈ Z with T(z') = (b, (T z).2).

Русский

Локальный подьём через тривиализацию T отправляет пару (z, b) в уникальное z' ∈ Z такой, что T(z') = (b, компонент2(T z)).

LaTeX

$$$$\mathrm{lift}_T(z,b)=T^{-1}\bigl(b,\, (T z)_2\bigr).$$$$

Lean4

/-- The local lifting through a Trivialization `T` from the base to the leaf containing `z`. -/
def lift (T : Trivialization F proj) (z : Z) (b : B) : Z :=
  T.invFun (b, (T z).2)

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