factorsThru_of_le

Mathlib.CategoryTheory.Sites.Coverage

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.factorsThru_of_le

English

If S ≤ T, then S.FactorsThru T.

Русский

Если S ⊆ T, то S.FactorsThru T.

LaTeX

$$$S \le T \Rightarrow S.FactorsThru T$$$

Lean4

theorem factorsThru_of_le {X : C} (S T : Presieve X) (h : S ≤ T) : S.FactorsThru T := fun Y g hg =>
  ⟨Y, 𝟙 _, g, h _ hg, by simp⟩

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

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

Разделы

Аффилиация

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