le_of_factorsThru_sieve

Mathlib.CategoryTheory.Sites.Coverage

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

Lean4

theorem le_of_factorsThru_sieve {X : C} (S : Presieve X) (T : Sieve X) (h : S.FactorsThru T) : S ≤ T :=
  by
  rintro Y f hf
  obtain ⟨W, i, e, h1, rfl⟩ := h hf
  exact T.downward_closed h1 _

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

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

Разделы

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

Аффилиация

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