apply_symm_apply' — Mathlib

English

Let e be a pretrivialization. If b lies in the base set of e, then applying e to the inverse of the local chart at (b, x) recovers the original pair (b, x) for every x in the fiber F.

Русский

Пусть e — предварительная тривиализация. Пусть b принадлежит базовому множеству e. Тогда применение e к обратному отображению локальной карты в координатах (b, x) восстанавливает исходную пару (b, x) для всякого x в F.

LaTeX

$$$\forall b\in e.baseSet\, \forall x\in F, e\left(e.toPartialEquiv.symm (b,x)\right)=(b,x) $$$

Lean4

theorem apply_symm_apply' {b : B} {x : F} (hx : b ∈ e.baseSet) : e (e.toPartialEquiv.symm (b, x)) = (b, x) :=
  e.apply_symm_apply (e.mem_target.2 hx)

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