toSpecΓ_top — Mathlib

English

The top open's toSpecΓ equals inclusion composed with X.toSpecΓ.

Русский

Для верхнего открытого множества его toSpecΓ равен композиции включения и X.toSpecΓ.

LaTeX

$$$$ (\top : X.\text{Opens}).\text{toSpecΓ} = (\top : X.\text{Opens}).\iota \circ X.\text{toSpecΓ}. $$$$

Lean4

@[simp]
theorem toSpecΓ_top {X : Scheme} : (⊤ : X.Opens).toSpecΓ = (⊤ : X.Opens).ι ≫ X.toSpecΓ := by
  simp [Scheme.Opens.toSpecΓ, toSpecΓ_naturality]; rfl

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