Theorems · Theorem · general topology

isLocallyClosed_tfae

∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X),
  [IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ nhds x, IsClosed (Subtype.val ⁻¹' s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (Subtype.val ⁻¹' s)].TFAE

A set s is locally closed if one of the equivalent conditions below hold 1. It is the intersection of some open set and some closed set. 2. The coborder (closure s \ s)ᶜ is open. 3. s is closed in some neighborhood of x for all x ∈ s. 4. Every x ∈ s has some open neighborhood U such that U ∩ closure s ⊆ s. 5. s is open in the closure of s.

Defined in

Mathlib.Topology.LocallyClosed

Cited by

2 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace