isQuasiSeparated — Mathlib

English

If U is an affine open in a scheme X, then the open subset U, viewed as a topological space, is quasi-separated.

Русский

Если U является аффинным открытым подпостроением X, то U как топологическое пространство квазиразделимо.

LaTeX

$$$\\text{IsAffineOpen}(U) \\Rightarrow \\mathrm{IsQuasiSeparated}(U).$$$

Lean4

theorem isQuasiSeparated {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : IsQuasiSeparated (U : Set X) :=
  by
  rw [isQuasiSeparated_iff_quasiSeparatedSpace]
  exacts [@AlgebraicGeometry.quasiSeparatedSpace_of_isAffine _ hU, U.isOpen]

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