Module

CompactOpenSpecialization.lean

Nyll.SchemeTheory.LocalGeometry.CompactOpenSpecialization

1 declaration indexed from sourceView source ↗

Module documentation

Avoiding a compact open set by a neighborhood

The proof takes a finite constructible-open cover of the compact open set by complements of compact open neighborhoods of the specified point.

Imports8

Mathlib.Topology.Basic
Mathlib.Topology.Compactness.Compact
Mathlib.Topology.Inseparable
Mathlib.Topology.Sets.Opens
Mathlib.Topology.Spectral.Basic
Mathlib.Topology.Spectral.ConstructibleTopology
Mathlib.Topology.Spectral.Prespectral
Mathlib.Topology.WithTopology

Imported by2

theorem

exists_open_nhds_disjoint_of_forall_not_specializes

L29 ↗

Documentation

A compact open set in a spectral space can be avoided by an open neighborhood of a point if none of its points specializes to that point.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TopologicalSpace Topology
universe u

Lean source · statement

theorem exists_open_nhds_disjoint_of_forall_not_specializes
    {X : Type u} [TopologicalSpace X] [SpectralSpace X]
    (K : Set X) (hKopen : IsOpen K) (hKcompact : IsCompact K)
    (x : X) (havoid : ∀ y ∈ K, ¬ y ⤳ x) :
    ∃ V : Opens X, x ∈ V ∧ Disjoint (V : Set X) K

Module documentation

Avoiding a compact open set by a neighborhood

Declarations

exists_open_nhds_disjoint_of_forall_not_specializes