functorPushforward_monotone

Mathlib.CategoryTheory.Sites.Sieves

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

← MathLib Explorer

English

For any F and X, the map Sieve.functorPullback F is monotone.

Русский

Для любого F моя карта Sieve.functorPullback F монотонна.

LaTeX

$$$ \\text{Monotone}(\\mathrm{Sieve}.\\mathrm{functorPullback} F) $$$

Lean4

theorem functorPushforward_monotone (X : C) : Monotone (Sieve.functorPushforward F : Sieve X → Sieve (F.obj X)) :=
  (functor_galoisConnection F X).monotone_l

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

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

Разделы

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

Аффилиация

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