Theorems · Theorem · general topology

IsCompact.binary_compact_cover

∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {K U V : Set X},
  IsCompact K → IsOpen U → IsOpen V → K ⊆ U ∪ V → ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

If a compact set is covered by two open sets, then we can cover it by two compact subsets.

Defined in

Mathlib.Topology.Separation.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceR1Space