Theorems · Theorem · general topology

closure_pi_set

∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (α i)] (I : Set ι) (s : (i : ι) → Set (α i)),
  closure (I.pi s) = I.pi fun i => closure (s i)

Defined in

Mathlib.Topology.NhdsWithin

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpace