Theorems · Theorem · Lie groups

RestrictedProduct.nhds_eq_map_inclusion

∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ {S : Set ι} (hS : Filter.cofinite ≤ Filter.principal S)
      (x : RestrictedProduct (fun i => R i) (fun i => A i) (Filter.principal S)),
      nhds (RestrictedProduct.inclusion R A hS x) = Filter.map (RestrictedProduct.inclusion R A hS) (nhds x)

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpace