pullbackIsoProdSubtype_hom_apply — Mathlib

English

The forward map of the isomorphism applied to a pullback element x yields the pair made from the forward projections fst and snd of x.

Русский

Проведя по изоморфизму от элемента пределa x вперёд, получаем пару, составленную из проекций fst и snd применённых к x.

LaTeX

$$$ (pullbackIsoProdSubtype f g).hom x = \langle\langle pullback.fst f g x, pullback.snd f g x\rangle, \text{proof of equality} \rangle $$$

Lean4

theorem pullbackIsoProdSubtype_hom_apply {f : X ⟶ Z} {g : Y ⟶ Z} (x : ↑(pullback f g)) :
    (pullbackIsoProdSubtype f g).hom x =
      ⟨⟨pullback.fst f g x, pullback.snd f g x⟩, by simpa using CategoryTheory.congr_fun pullback.condition x⟩ :=
  rfl

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