Theorems · Theorem · general topology
Filter.HasBasis.prod_self
∀ {α : Type u_1} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α},
la.HasBasis pa sa → (la ×ˢ la).HasBasis pa fun i => sa i ×ˢ sa i- Defined in
- Mathlib.Order.Filter.Bases.Basic
- Cited by
- 19 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.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Filterstatement and proof · cited by 8,121
- SProd.sprodstatement · cited by 1,750
- Filter.HasBasisstatement and proof · cited by 604
- Filter.HasBasis.mem_iffproof · cited by 193
- Filter.inter_memproof · cited by 153
- Filter.HasBasis.mem_of_memproof · cited by 63
- Filter.HasBasis.prod_same_indexproof · cited by 3
Cited by19
Results whose statement or proof uses this declaration.
- Filter.HasBasis.cauchySeq_iffproof · cited by 5
- Filter.mem_prod_self_iffproof · cited by 4
- Filter.HasBasis.cauchy_iffproof · cited by 3
- exists_nhds_squareproof · cited by 3
- nhdsSet_diagonal_eq_uniformityproof · cited by 2
- AddGroupFilterBasis.cauchy_iffproof · cited by 2
- IsGδ.setOfPred_continuousAtproof · cited by 2
- Metric.isBounded_range_of_tendsto_cofinite_uniformityproof · cited by 2
- IsSeqCompact.isCompleteproof · cited by 1
- Filter.HasBasis.add_selfproof · cited by 1
- BoxIntegral.integrable_iff_cauchy_basisproof · cited by 1
- Filter.eventually_atBot_prod_selfproof · cited by 1