def SeparatedHausdorffClassical.complexPoints (X : AlgebraicGeometry.Scheme) : Type

Complex points of a scheme X: morphisms Spec ℂ → X.

noncomputable def SeparatedHausdorffClassical.classicalTopology (X : AlgebraicGeometry.Scheme) (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of ℂ)) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.IsReduced X] : TopologicalSpace (complexPoints X)

The classical (analytic / Hausdorff) topology on the complex points of a reduced, locally-finite-type ℂ-scheme.

theorem SeparatedHausdorffClassical.separated_iff_hausdorff_classical {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of ℂ)) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.IsReduced X] : X.IsSeparated ↔ T2Space (complexPoints X)

A reduced, locally-finite-type ℂ-scheme is separated iff its complex points form a Hausdorff space in the classical topology.