naturality_inv

Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Monoidal.naturality_inv

Lean4

theorem naturality_inv {p f g pf : C} {η : f ≅ g} (η_f : p ⊗ f ≅ pf) (η_g : p ⊗ g ≅ pf) (ih : p ◁ η ≪≫ η_g = η_f) :
    p ◁ η.symm ≪≫ η_f = η_g := by
  rw [← ih]
  apply Iso.ext
  simp

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

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

Разделы

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

Аффилиация

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