AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_isOpen_isIrreducible_nhd.SmoothUnibranchAux.isOpen_connectedComponent_of_noetherianSpace
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_isOpen_isIrreducible_nhd
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace SmoothUnibranchAuxLean source · statement
theorem isOpen_connectedComponent_of_noetherianSpace {α : Type*} [TopologicalSpace α]
[TopologicalSpace.NoetherianSpace α] (x : α) : IsOpen (connectedComponent x)