flip_injective

Mathlib.CategoryTheory.Functor.Currying

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.flip_injective

English

If F1.flip = F2.flip, then F1 = F2.

Русский

Если F1.flip равно F2.flip, то F1 равно F2.

LaTeX

$$$F_1^{\text{flip}} = F_2^{\text{flip}} \Rightarrow F_1 = F_2$$$

Lean4

theorem flip_injective {F₁ F₂ : B ⥤ C ⥤ D} (h : F₁.flip = F₂.flip) : F₁ = F₂ := by
  rw [← flip_flip F₁, ← flip_flip F₂, h]

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

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

Разделы

Аффилиация

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