English
Evaluation of the concrete const construction matches IsLocalization.mk' evaluation at x.
Русский
Вычисление константной конструкции совпадает с IsLocalization.mk' в точке x.
LaTeX
$$$\\text{const\\_apply}\\;R\\;f\\;g\\;U\\;\\hu(x) : ((\\mathrm{const}\\;R\\;f\\;g\\;U\\;\\hu).1\\; x) = \\mathrm{IsLocalization.mk'}(\\mathrm{Localization.AtPrime}\\;x.1.asIdeal)\\; f\\; \\langle g,\\ hu\\ x x.2\\rangle$$$
Lean4
@[simp]
theorem const_apply (f g : R) (U : Opens (PrimeSpectrum.Top R))
(hu : ∀ x ∈ U, g ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) (x : U) :
(const R f g U hu).1 x = IsLocalization.mk' (Localization.AtPrime x.1.asIdeal) f ⟨g, hu x x.2⟩ :=
rfl