congr_left

Mathlib.CategoryTheory.Comma.Arrow

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Arrow.hom.congr_left

English

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

Русский

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

LaTeX

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

Lean4

theorem congr_left {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.left = φ₂.left := by rw [h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru