Theorems · Theorem · general topology

isOpen_pi_iff

∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {s : Set ((a : ι) → A a)},
  IsOpen s ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s

Defined in

Mathlib.Topology.Constructions

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpace