of_hom

Mathlib.CategoryTheory.IsConnected

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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