Theorems · Theorem · Lie groups

RestrictedProduct.nhds_zero_eq_map_ofPre

∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {T : Set ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → Zero (R i)]
  [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (R i)],
  (∀ (i : ι), IsOpen ↑(B i)) →
    ∀ (hT : Filter.cofinite ≤ Filter.principal T),
      nhds (RestrictedProduct.inclusion R (fun i => ↑(B i)) hT 0) =
        Filter.map (RestrictedProduct.inclusion R (fun i => ↑(B i)) hT) (nhds 0)

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

SetLikeTopologicalSpaceZeroZeroMemClass