germ_toOpen — Mathlib

English

An extensionality principle for fractions shows equality of const representations when the cross-multiplication matches.

Русский

Принцип эктенциализации для дробей: равенство константных представлений при равенстве перемножаемых поперек.

LaTeX

$$$ f_1 g_2 = f_2 g_1 \\Rightarrow const_R f_1 g_1 = const_R f_2 g_2 $$$

Lean4

@[simp]
theorem germ_toOpen (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) (hx : x ∈ U) (f : R) :
    (structureSheaf R).presheaf.germ U x hx (toOpen R U f) = toStalk R x f := by rw [← toOpen_germ]; rfl

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