pushoutCocone_inl_eq_inr_iff_of_iso

English

Let c and c' be pushout cocones of f and g, and e: c ≅ c'. Then c.inl x1 = c.inr x2 if and only if c'.inl x1 = c'.inr x2, for all x1 ∈ X1 and x2 ∈ X2.

Русский

Пусть c и c' — пушаут-коконы для f и g, и e: c ≅ c'. Тогда выполнено равенство c.inl x1 = c.inr x2 эквивалентно c'.inl x1 = c'.inr x2 для всех x1 ∈ X1 и x2 ∈ X2.

LaTeX

$$$\\forall {f:S \\to X_1}\\, {g:S \\to X_2}\\;\\forall {c,c':PushoutCocone f g}\\; (e:c \\cong c')\\; (x_1:X_1) (x_2:X_2):\\; c.inl x_1 = c.inr x_2 \\iff c'.inl x_1 = c'.inr x_2$$$

Lean4

theorem pushoutCocone_inl_eq_inr_iff_of_iso {c c' : PushoutCocone f g} (e : c ≅ c') (x₁ : X₁) (x₂ : X₂) :
    c.inl x₁ = c.inr x₂ ↔ c'.inl x₁ = c'.inr x₂ := by
  constructor
  · apply pushoutCocone_inl_eq_inr_imp_of_iso e
  · apply pushoutCocone_inl_eq_inr_imp_of_iso e.symm

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