res_const' — Mathlib

English

A variant of res_const with a particular choice of the base opens; the restricted const R f g on a basic open equals the same fractional expression on that basic open.

Русский

Вариант свойства ограничения константы на базовом открытом множестве: ограниченная константа на базовом открытом равна той же дроби на этом открытом.

LaTeX

$$$ (structureSheaf R).1.map (homOfLE hv).op (const R f g (PrimeSpectrum.basicOpen g) ...) = const R f g V hv $$$

Lean4

theorem res_const' (f g : R) (V hv) :
    (structureSheaf R).1.map (homOfLE hv).op (const R f g (PrimeSpectrum.basicOpen g) fun _ => id) = const R f g V hv :=
  rfl

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