exists_of_res_eq_of_qcqs_of_top — Mathlib

English

In the topological setting, if f and g agree on a basic open of the top space, there exists n with s^n f = s^n g after localization.

Русский

В топологическом контексте, если f и g согласованы на базовом открытом над топологическим пространством, существует n: s^n f = s^n g после локализации.

LaTeX

$$$$\\exists n, s^{n} \\cdot f = s^{n} \\cdot g$$$$

Lean4

theorem exists_of_res_eq_of_qcqs_of_top {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X] {f g s : Γ(X, ⊤)}
    (hfg : f |_ X.basicOpen s = g |_ X.basicOpen s) : ∃ n, s ^ n * f = s ^ n * g :=
  exists_of_res_eq_of_qcqs (U := ⊤) CompactSpace.isCompact_univ isQuasiSeparated_univ hfg

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