Theorems · Theorem · general topology
nhds_pi
∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {a : (i : ι) → A i},
nhds a = Filter.pi fun i => nhds (a i)- Defined in
- Mathlib.Topology.Constructions
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- iInfproof · cited by 1,690
- Filter.comapproof · cited by 546
- Function.evalproof · cited by 140
- Filter.pistatement · cited by 48
- nhds_inducedproof · cited by 32
- nhds_iInfproof · cited by 14
Cited by29
Results whose statement or proof uses this declaration.
- tendsto_pi_nhdsproof · cited by 58
- isOpen_pi_iffproof · cited by 6
- MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendstoproof · cited by 5
- isCompact_pi_infiniteproof · cited by 3
- inseparable_piproof · cited by 2
- Topology.IsInducing.piMapproof · cited by 2
- Asymptotics.IsLittleOTVS.piproof · cited by 1
- Asymptotics.IsBigOTVS.piproof · cited by 1
- Function.Surjective.isEmbedding_compproof · cited by 1
- set_pi_mem_nhds_iffproof · cited by 1
- Metric.PiNatEmbed.continuous_distDenseSeq_invproof · cited by 1
- nhdsKer_singleton_piproof · cited by 1