symm_apply_mk_proj — Mathlib

English

Let e be a trivialization. For any x with x in the source of e, applying the inverse of the associated open partial homeomorph to the pair (proj x, (e x).2) yields x. In symbols, e.toOpenPartialHomeomorph.symm(proj x, (e x).2) = x for ex.

Русский

Пусть e — тривиализация. Для всякой точки x, принадлежащей области определения, обратное отображение открытого частичного гомеоморфа, примененное к паре (proj x, (e x).2), возвращает x: e.toOpenPartialHomeomorph.symm(proj x, (e x).2) = x.

LaTeX

$$$\forall x\,(x \in e.source)\;\, e.toOpenPartialHomeomorph.symm(\operatorname{proj} x, (e x).2) = x$$$

Lean4

@[simp, mfld_simps]
theorem symm_apply_mk_proj (ex : x ∈ e.source) : e.toOpenPartialHomeomorph.symm (proj x, (e x).2) = x :=
  e.toPretrivialization.symm_apply_mk_proj ex

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