const_apply — Mathlib

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

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