Theorems · Theorem · general topology

Set.Finite.dense_sInter

∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (Set X)},
  s.Finite → (∀ t ∈ s, IsOpen t) → (∀ t ∈ s, Dense t) → Dense (⋂₀ s)

The intersection of finitely many open dense sets is dense.

Defined in

Mathlib.Topology.Baire.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace