symm_apply_mk_proj — Mathlib

English

If x is in the source, then the inverse map applied to the pair (proj x, (e x)2) yields x, i.e., the projection and the second component come back together.

Русский

Если x лежит в области определения, то применение обратного отображения к паре (proj x, (e x)2) даёт x.

LaTeX

$$$\forall x\in e.source\, e.toPartialEquiv.symm (proj x, (e x)_{2})=x$$$

Lean4

@[simp, mfld_simps]
theorem symm_apply_mk_proj {x : Z} (ex : x ∈ e.source) : e.toPartialEquiv.symm (proj x, (e x).2) = x := by
  rw [← e.coe_fst ex, ← e.coe_coe, e.left_inv ex]

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