pullback_monotone

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sieve.pullback_monotone

English

For a fixed arrow f, the map S ↦ S.pullback f is monotone with respect to inclusion of sieves.

Русский

Для фиксированного стрелка f отображение S ↦ S.pullback f неубывающе по включению сит.

LaTeX

$$$ S \\le T \\Rightarrow S.pullback f \\le T.pullback f $$$

Lean4

theorem pullback_monotone (f : Y ⟶ X) : Monotone (Sieve.pullback f) :=
  (galoisConnection f).monotone_u

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

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

Разделы

Аффилиация

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