res_const — Mathlib

English

For any f,g in R and opens U⊆PrimeSpectrum.Top R with suitable nonvanishing conditions hu, hv, the restriction of the constant section const_R f g U hu along i: V→U equals the constant section on V: const_R f g V hv.

Русский

Для любых элементов f,g ∈ R и открытых множеств U ⊆ Spec(R) при допустимых условиях ненулевости hu, hv ограничение константной секции const_R f g U hu по отображению i: V→U равно константной секции на V: const_R f g V hv.

LaTeX

$$$ (structureSheaf R).1.map i (const R f g U hu) = const R f g V hv $$$

Lean4

@[simp]
theorem res_const (f g : R) (U hu V hv i) : (structureSheaf R).1.map i (const R f g U hu) = const R f g V hv :=
  rfl

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