tgt

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.tgt

English

Another transitivity variant of MapEq for nested indices.

Русский

Другая вариация транзитивности MapEq для вложенных индексов.

LaTeX

$$$ \\text{MapEq } F G k_1 k_3 h_{12} h_3 \\Rightarrow \\text{MapEq } F G k_1 k_3 h_{12} h_3 $$$

Lean4

theorem tgt : F.obj ⟨k₂, h₂⟩ = G.obj ⟨k₂, h₂⟩ :=
  congr_arg Comma.right h

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

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

Разделы

Аффилиация

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