toΓSpecCApp_spec — Mathlib

English

The equation relating the open restriction maps and the CApp construction holds on basic opens.

Русский

Уравнение, связывающее ограничивающие отображения и конструирование CApp на базовых открытых множеств.

LaTeX

$$$toOpen(Γ(X), basicOpen(r)) \circ f = X.toToΓSpecMapBasicOpen(r) \Rightarrow f = X.toΓSpecCApp(r)$$$

Lean4

theorem toΓSpecCApp_spec : toOpen _ (basicOpen r) ≫ X.toΓSpecCApp r = X.toToΓSpecMapBasicOpen r :=
  (X.toΓSpecCApp_iff r _).2 rfl

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