Theorems · Theorem · general topology
Filter.nhds_iInf
∀ {ι : Sort u_1} {α : Type u_2} (f : ι → Filter α), nhds (⨅ i, f i) = ⨅ i, nhds (f i)- Defined in
- Mathlib.Topology.Filter
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Filterstatement and proof · cited by 8,121
- nhdsstatement · cited by 5,554
- Set.univproof · cited by 3,945
- iInfstatement and proof · cited by 1,690
- Set.Iicproof · cited by 1,111
- Filter.principalproof · cited by 740
- Filter.principal_univproof · cited by 46
- Filter.inf_principalproof · cited by 29
- Set.Iic_topproof · cited by 10
- Set.Iic_inter_Iicproof · cited by 9
- Filter.nhds_eqproof · cited by 6
Cited by2
Results whose statement or proof uses this declaration.
- Filter.nhds_atTopproof · cited by 2
- Filter.nhds_infproof · cited by 1