comap_map_le

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.IdealSheafData.comap_map_le

English

A convenience equivalence showing comap_map_le holds at the level of partial orders.

Русский

Упрощенная версия равенства comap_map_le в рамках частичных порядков.

LaTeX

$$(I.map f).comap f ≤ I$$

Lean4

theorem comap_map_le : (I.map f).comap f ≤ I :=
  (map_gc f).l_u_le I

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

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

Разделы

Аффилиация

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