map_inf

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

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

English

Another expression that map of the top equals top

Русский

Еще одно выражение: map верхнего элемента = верхний элемент.

LaTeX

$$map ⊤ f = ⊤$$

Lean4

@[simp]
theorem map_inf : map (I₁ ⊓ I₂) f = map I₁ f ⊓ map I₂ f :=
  (map_gc f).u_inf

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

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

Разделы

Аффилиация

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