of_inv

Mathlib.CategoryTheory.IsConnected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Zag.of_inv

English

If there is a morphism f: j2 → j1, then Zag j1 j2 holds.

Русский

Если существует морфизм f: j2 → j1, то Zag(j1, j2) выполняется.

LaTeX

$$$\forall j_1 j_2,\ (f : j_2 \to j_1) \Rightarrow Zag(j_1,j_2)$$$

Lean4

theorem of_inv {j₁ j₂ : J} (f : j₂ ⟶ j₁) : Zag j₁ j₂ :=
  Or.inr ⟨f⟩

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

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

Разделы

Аффилиация

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