Theorems · Theorem · general topology

Dense.induction

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  Dense s → ∀ {P : X → Prop}, (∀ x ∈ s, P x) → IsClosed {x | P x} → ∀ (x : X), P x

If a closed property holds for a dense subset, it holds for the whole space.

Defined in

Mathlib.Topology.Closure

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace