toOpen_apply — Mathlib

English

Equating toOpen with a const-section of the form const_R f 1 on an open recovers the correct algebra map evaluation.

Русский

Равенство toOpen и константной секции вида const_R f 1 на открытом множестве восстанавливает корректную оценку алгебраического отображения.

LaTeX

$$$ toOpen\\_R U f = const\\_R f 1 U \\dots $$$

Lean4

@[simp]
theorem toOpen_apply (U : Opens (PrimeSpectrum.Top R)) (f : R) (x : U) : (toOpen R U f).1 x = algebraMap _ _ f :=
  rfl

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