factors_left_of_inf_factors

Mathlib.CategoryTheory.Subobject.Lattice

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.factors_left_of_inf_factors

← MathLib Explorer

English

The left factor through the arrow (X ⊓ Y).arrow exists; the arrow factors through X.

Русский

Существование разложения стрелы (X ⊓ Y).arrow через X.

LaTeX

$$$ \\exists i: (X \\cap Y) \\to X,\\ (X \\cap Y).arrow = X.arrow \\circ i $$$

Lean4

theorem factors_left_of_inf_factors {A B : C} {X Y : Subobject B} {f : A ⟶ B} (h : (X ⊓ Y).Factors f) : X.Factors f :=
  factors_of_le _ (inf_le_left _ _) h

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

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

Разделы

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

Аффилиация

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