mk_symm — Mathlib

English

The total-space element corresponding to the base point b and the symmetric fiber value e.symm b y is exactly the image of (b, y) under the inverse of the local trivialization.

Русский

Элемент общего пространства, соответствующий основанию b и симметрическому значению волокна, равен обратному образу (b, y) через локальную тривиализацию.

LaTeX

$$$\\mathrm{TotalSpace}.mk\\, b\\, (e.symm\\, b\\, y) = e.toOpenPartialHomeomorph.symm (b, y)$$$

Lean4

theorem mk_symm (e : Trivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) :
    TotalSpace.mk b (e.symm b y) = e.toOpenPartialHomeomorph.symm (b, y) :=
  e.toPretrivialization.mk_symm hb y

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