Theorems · Theorem · general topology

isClosed_set_pi

∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {i : Set ι} {s : (a : ι) → Set (A a)},
  (∀ a ∈ i, IsClosed (s a)) → IsClosed (i.pi s)

Defined in

Mathlib.Topology.Constructions

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpace