Theorems · Definition · general topology
Filter.pi
{ι : Type u_3} → {α : ι → Type u_4} → ((i : ι) → Filter (α i)) → Filter ((i : ι) → α i)The product of an indexed family of filters.
- Defined in
- Mathlib.Order.Filter.Defs
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement and proof · cited by 8,121
- iInfproof · cited by 1,690
- Filter.comapproof · cited by 546
- Function.evalproof · cited by 140
Cited by48
Results whose statement or proof uses this declaration.
- nhds_pistatement · cited by 29
- Filter.mem_pistatement · cited by 8
- Filter.tendsto_pistatement · cited by 7
- Filter.hasBasis_pistatement and proof · cited by 5
- Filter.pi_mem_pistatement and proof · cited by 4
- Filter.tendsto_eval_pistatement · cited by 4
- Filter.le_pistatement · cited by 2
- Filter.mem_of_pi_mem_pistatement and proof · cited by 2
- Filter.mem_pi_of_memstatement · cited by 2
- Filter.pi_inf_principal_univ_pi_eq_botstatement · cited by 2
- Filter.pi_monostatement · cited by 2
- Filter.map_eval_pistatement and proof · cited by 2