mapEq_refl

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

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

← MathLib Explorer

English

If for all k1 ≤ k2 we have MapEq F G k1 k2 with witnesses, then F = G.

Русский

Если для всех k1 ≤ k2 имеются соответствие MapEq F G, тогда F = G.

LaTeX

$$$ F = G $$$

Lean4

theorem mapEq_refl (k : K) (hk : k ≤ x) (h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩) : MapEq F G k k (by simp) hk := by
  rw [MapEq, arrowMap_refl, arrowMap_refl, h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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