Theorems · Theorem · general topology

nhdsWithin_pi_eq

∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] {I : Set ι},
  I.Finite →
    ∀ (s : (i : ι) → Set (X i)) (x : (i : ι) → X i),
      nhdsWithin x (I.pi s) =
        (⨅ i ∈ I, Filter.comap (fun x => x i) (nhdsWithin (x i) (s i))) ⊓
          ⨅ i, ⨅ (_ : i ∉ I), Filter.comap (fun x => x i) (nhds (x i))

Defined in

Mathlib.Topology.NhdsWithin

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace