Theorems · Theorem · general topology

PiNat.isOpen_iff_dist

∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  (s : Set ((n : ℕ) → E n)), IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDiscreteTopology