ext_to_iff — Mathlib

English

Let Z be an object and f,g : Z → X ⊞ Y a pair of morphisms into a binary biproduct X ⊞ Y. Then f = g if and only if their projections to X and to Y coincide, i.e. f ; fst = g ; fst and f ; snd = g ; snd.

Русский

Пусть Z — некоторый объект, а f,g : Z → X ⊞ Y — пара морфизмов в бинарный биопродукт X ⊞ Y. Тогда выполняется: f = g тогда и только если их проекции на X и на Y совпадают, то есть f ≫ fst = g ≫ fst и f ≫ snd = g ≫ snd.

LaTeX

$$$f = g \iff f \circ \pi_1 = g \circ \pi_1 \;\land\; f \circ \pi_2 = g \circ \pi_2,$$$

Lean4

theorem ext_to_iff {f g : Z ⟶ X ⊞ Y} : f = g ↔ f ≫ biprod.fst = g ≫ biprod.fst ∧ f ≫ biprod.snd = g ≫ biprod.snd := by
  aesop

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