pullbackMk_fst — Mathlib

English

For x1 ∈ X1, x2 ∈ X2 and h: f1 x1 = f2 x2, the first projection of the pullbackMk object recovers x1.

Русский

Для x1 ∈ X1, x2 ∈ X2 и h: f1 x1 = f2 x2, первая проекция pullbackMk возвращает x1.

LaTeX

$$$pullback.fst\ f_1\ f_2\\ (pullbackMk\ f_1\ f_2\\ x_1\\ x_2\\ h) = x_1$$$

Lean4

@[simp]
theorem pullbackMk_fst (x₁ : ToType X₁) (x₂ : ToType X₂) (h : f₁ x₁ = f₂ x₂) :
    pullback.fst f₁ f₂ (pullbackMk f₁ f₂ x₁ x₂ h) = x₁ :=
  (congr_fun (PreservesPullback.iso_inv_fst (forget C) f₁ f₂) _).trans
    (congr_fun (Types.pullbackIsoPullback_inv_fst ⇑(ConcreteCategory.hom f₁) ⇑(ConcreteCategory.hom f₂)) _)

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