map_comap_le

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.map_comap_le

English

For any map m: α → β and any filter g on β, the image of the pullback of g along m is below g: map m (comap m g) ≤ g.

Русский

Для любой отображения m: α → β и любого фильтра g на β образ: m(комап m g) ≤ g.

LaTeX

$$$ \\operatorname{map}_m(\\operatorname{comap}_m g) \\le g $$$

Lean4

theorem map_comap_le : map m (comap m g) ≤ g :=
  (gc_map_comap m).l_u_le _

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

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

Разделы

Аффилиация

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