fromSpecStalk_eq_fromSpecStalk — Mathlib

English

The morphisms fromSpecStalk associated to different affine neighborhoods of x coincide; i.e., the construction is independent of the chosen affine neighborhood, as long as hxU and hxV hold.

Русский

Морфизм fromSpecStalk, соответствующий различным а AFF-окрестностям x, совпадает.

LaTeX

$$theorem fromSpecStalk_eq_fromSpecStalk {x : X} (hxU : x ∈ U) : hU.fromSpecStalk hxU = X.fromSpecStalk x$$

Lean4

@[simp]
theorem fromSpecStalk_eq_fromSpecStalk {x : X} (hxU : x ∈ U) : hU.fromSpecStalk hxU = X.fromSpecStalk x :=
  fromSpecStalk_eq ..

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