English
Let e be a trivialization of the bundle with projection π and fiber F. If a base point x lies in the base set of e, then the first coordinate of the inverse of the local trivialization at (x, y) is x; i.e. the inverse map preserves the base coordinate on its domain.
Русский
Пусть e — тривиализация расслоения с проекцией π и волокном F. Если точка x принадлежит базовому множеству e, тогда первая координата обратной локальной гомоморфной карты в (x, y) равна x; то есть обратная карта сохраняет базовую координату на своей области определения.
LaTeX
$$$\\pi_1\\big( e.toOpenPartialHomeomorph.symm (x, y) \\big) = x$ on $x \\in e.baseSet$, i.e. $ (e.toOpenPartialHomeomorph.symm (x, y)).fst = x $$$
Lean4
@[simp, mfld_simps]
theorem symm_coe_proj {x : B} {y : F} (e : Trivialization F (π F E)) (h : x ∈ e.baseSet) :
(e.toOpenPartialHomeomorph.symm (x, y)).1 = x :=
e.proj_symm_apply' h
