map_ideal' — Mathlib

English

A form of map_ideal that is convenient to rewrite: for any I and morphism h, the corresponding equality holds.

Русский

Упрощённая форма map_ideal, удобная для проставления: для любого I и отображения h выполняется равенство.

LaTeX

$$$ (I.ideal V).map (X.presheaf.map h).hom = I.ideal U $$$

Lean4

/-- A form of `map_ideal` that is easier to rewrite with. -/
theorem map_ideal' {U V : X.affineOpens} (h : Opposite.op V.1 ⟶ .op U.1) :
    (I.ideal V).map (X.presheaf.map h).hom = I.ideal U :=
  map_ideal _ _

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