English
Let e be a trivialization of a bundle with projection proj. If b lies in the base set of e, then applying the inverse of the associated partial homeomorphism to the pair (b, x) returns (b, x) for every x in the fiber. In symbols, e(e.toOpenPartialHomeomorph.symm(b, x)) = (b, x) whenever b ∈ e.baseSet.
Русский
Пусть e — тривиализация фибры с проекцией proj. Если b принадлежит базовому множеству e, то применение обратного отображения частичной гомеоморфии к паре (b, x) возвращает (b, x) для любого x из фибры: e(e.toOpenPartialHomeomorph.symm(b, x)) = (b, x), когда b ∈ e.baseSet.
LaTeX
$$$\forall b\in e.baseSet, \forall x,\ e( e.toOpenPartialHomeomorph.symm(b, x) ) = (b, x).$$$
Lean4
theorem apply_symm_apply' {b : B} {x : F} (hx : b ∈ e.baseSet) : e (e.toOpenPartialHomeomorph.symm (b, x)) = (b, x) :=
e.toPretrivialization.apply_symm_apply' hx
