toOpenPartialHomeomorph_trivialization_symm_apply

English

There exists a canonical open partial homeomorphism structure between the trivialization and the projection on the base.

Русский

Существует каноническое открытое частичное гомеоморфизм между тривиализацией и проекцией на основание.

LaTeX

$$$ (\mathrm{Bundle.Trivial.trivialization}\ B\ F).toOpenPartialHomeomorph \text{ is an open partial homeomorphism }$$$

Lean4

@[simp]
theorem toOpenPartialHomeomorph_trivialization_symm_apply (v : B × F) :
    (trivialization B F).toOpenPartialHomeomorph.symm v = ⟨v.1, v.2⟩ :=
  rfl

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