ofEpiOfIsIsoOfMono'_g'_τ₃ — Mathlib

English

For the primed construction, the g' component satisfies (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'.

Русский

Для примированной конструкции: (ofEpiOfIsIsoOfMono' φ h).g' ∘ φ.τ₃ = h.g'.

LaTeX

$$$ (\\mathrm{ofEpiOfIsIsoOfMono'}\\ φ\ h).g' \\circ φ.τ_3 = h.g' $$$

Lean4

@[simp]
theorem ofEpiOfIsIsoOfMono'_g'_τ₃ : (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g' := by
  rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p, assoc, p_g', φ.comm₂₃]

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