congr_right — Mathlib

English

Let f, g be arrows in T and φ1, φ2 : f ⟶ g. If φ1 = φ2, then φ1.right = φ2.right.

Русский

Пусть f, g — стрелы в T и φ1, φ2 : f ⟶ g. Если φ1 = φ2, то φ1.right = φ2.right.

LaTeX

$$$\forall f,g:(Arrow\ T)\;\forall \phi_1,\phi_2:(\phi_1:\,f\to g)\; (\phi_1 = \phi_2) \Rightarrow (\phi_1.right = \phi_2.right)$$$

Lean4

theorem congr_right {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.right = φ₂.right := by simp [h]

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