AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_exists_isClosed_irreducible_subset_fiber_of_not_quasiFiniteAt.P2mWs11C1.exists_isClosed_isIrreducible_ne_singleton
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_exists_isClosed_irreducible_subset_fiber_of_not_quasiFiniteAt
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mWs11C1Lean source · statement
theorem exists_isClosed_isIrreducible_ne_singleton {T : Type*} [TopologicalSpace T]
[TopologicalSpace.NoetherianSpace T]
(p : T) (hp : ¬ IsOpen ({p} : Set T)) :
∃ W : Set T, IsClosed W ∧ IsIrreducible W ∧ p ∈ W ∧ W ≠ {p}