Theorems · Theorem · general topology

QuasiSeparatedSpace.isCompact_sInter_of_nonempty

∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
  s.Finite → s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → IsCompact (⋂₀ s)

Defined in

Mathlib.Topology.QuasiSeparated

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceQuasiSeparatedSpace