prodEquiv_apply_fst — Mathlib

English

The first projection of prodEquiv applied to an element x is the underlying first projection evaluated at x.

Русский

Первая проекция prodEquiv применённого к элементу x равна базовой проекции x на X1.

LaTeX

$$$ (\\mathrm{prodEquiv} X_1 X_2 \\; x).\\text{fst} = (\\mathrm{Limits}.prod.fst) \\; x $$$

Lean4

@[simp]
theorem prodEquiv_apply_fst (x : ToType (X₁ ⨯ X₂)) : (prodEquiv X₁ X₂ x).fst = (Limits.prod.fst : X₁ ⨯ X₂ ⟶ X₁) x :=
  congr_fun (prodComparison_fst (forget C) X₁ X₂) x

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