pushforward_monotone

Mathlib.CategoryTheory.Sites.Sieves

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

English

For a fixed morphism f, the map S ↦ S.pushforward f is monotone.

Русский

Для фиксированного морфизма f отображение S ↦ S.pushforward f монотонно.

LaTeX

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

Lean4

theorem pushforward_monotone (f : Y ⟶ X) : Monotone (Sieve.pushforward f) :=
  (galoisConnection f).monotone_l

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

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

Разделы

Аффилиация

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