def ZariskiClosed (k : Type u_1) [Field k] (n : ℕ) (S : Set (Fin n → k)) : Prop

Zariski-closed subset of k^n over an algebraically closed k: a set cut out by the common vanishing of a (radical) ideal of polynomials (cf. Thm 1.2 identifying closed sets with radical ideals).

theorem exists_zariskiTopology (k : Type u_1) [Field k] [IsAlgClosed k] (n : ℕ) : ∃ (τ : TopologicalSpace (Fin n → k)), ∀ (S : Set (Fin n → k)), IsClosed S ↔ ZariskiClosed k n S

Zariski topology on affine space (Cor 1, Lec 1): there exists a topology on k^n whose closed sets are exactly the Zariski-closed subsets, exhibited by checking the closure axioms for the family of vanishing loci.