Theorems · Theorem · general topology

Filter.HasBasis.prod_same_index

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {sa : ι → Set α} {lb : Filter β} {p : ι → Prop}
  {sb : ι → Set β},
  la.HasBasis p sa →
    lb.HasBasis p sb →
      (∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j) → (la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i

Defined in

Mathlib.Order.Filter.Bases.Basic

Cited by

3 results in Mathlib

Foundations

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