English
If e is a trivialization and b lies in its base set, then the value of e.symm b y can be expressed via the second projection of the inverse of the open partial homeomorph and a casting from the fiber coordinate of the inverse of the local homeomorphism; i.e., e.symm b y equals the cast of the second component of e.toOpenPartialHomeomorph.symm (b, y) by the equality e.symm_coe_proj hb.
Русский
Если e — тривиализация и b ∈ базовое множество, то значение e.symm b y может быть записано через вторую координату обратной локальной гомоморфности и приведение по т.н. коэф. по e.symm_coe_proj hb.
LaTeX
$$$e.symm b y = \\text{cast} (\\operatorname{congr_arg}_E (e.symm\\_coe\\_proj hb)) ((e.toOpenPartialHomeomorph.symm (b, y)).2)$$$
Lean4
theorem symm_apply (e : Trivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) :
e.symm b y = cast (congr_arg E (e.symm_coe_proj hb)) (e.toOpenPartialHomeomorph.symm (b, y)).2 :=
dif_pos hb
