prodEquiv_symm_apply_snd — Mathlib

English

Under the same assumptions, the snd-projection after applying prodEquiv inverse gives the second coordinate: snd((prodEquiv X1 X2)^{-1} x) = x_2 for x=(x1,x2).

Русский

При тех же предпосылках snd((prodEquiv X1 X2)^{-1} x) = x_2 для x=(x1,x2).

LaTeX

$$$\\\\operatorname{snd}((\\\\mathrm{prodEquiv} \\\\ X_1 \\\\ X_2)^{-1} x) = x_2 \\\\text{with } x=(x_1,x_2)$$$

Lean4

@[simp]
theorem prodEquiv_symm_apply_snd (x : ToType X₁ × ToType X₂) :
    (Limits.prod.snd : X₁ ⨯ X₂ ⟶ X₂) ((prodEquiv X₁ X₂).symm x) = x.2 :=
  by
  obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x
  simp

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