ext_from_iff — Mathlib

English

For any morphisms f,g : X ⊞ Y → Z, f = g iff composing with the injections yields equality: inl ≫ f = inl ≫ g and inr ≫ f = inr ≫ g.

Русский

Для любых морфизмов f,g: X ⊞ Y → Z верно, что f = g тогда и только если inl ≫ f = inl ≫ g и inr ≫ f = inr ≫ g.

LaTeX

$$$f = g \iff (\iota_1 \circ f = \iota_1 \circ g) \land (\iota_2 \circ f = \iota_2 \circ g)$$$

Lean4

theorem ext_from_iff {f g : X ⊞ Y ⟶ Z} : f = g ↔ biprod.inl ≫ f = biprod.inl ≫ g ∧ biprod.inr ≫ f = biprod.inr ≫ g := by
  aesop

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