Theorems · Theorem · general topology

isIrreducible_iff_sUnion_isClosed

∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z

A set is irreducible if and only if for every cover by a finite collection of closed sets, it is contained in one of the members of the collection.

Defined in

Mathlib.Topology.Irreducible

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace