English
If f has a basis, then the product filter pi f has a natural basis built from it.
Русский
Если у f есть базис, то произведение Pi f имеет естественный базис, построенный на нем.
LaTeX
$$$\text{If } h: f.HasBasis(p,s), \text{ then } (\pi f) HasBasis (… )$$$
Lean4
theorem pi_self {α : Type*} {κ : Type*} {f : Filter α} {p : κ → Prop} {s : κ → Set α} (h : f.HasBasis p s) :
(pi fun _ ↦ f).HasBasis (fun Ik : Set ι × κ ↦ Ik.1.Finite ∧ p Ik.2) (fun Ik ↦ Ik.1.pi (fun _ ↦ s Ik.2)) :=
by
refine hasBasis_pi_same_index (fun _ ↦ h) (fun I k hI hk ↦ ?_)
rcases h.mem_iff.mp (biInter_mem hI |>.mpr fun i hi ↦ h.mem_of_mem (hk i hi)) with ⟨k₀, hk₀, hk₀'⟩
exact ⟨k₀, hk₀, fun i hi ↦ hk₀'.trans (biInter_subset_of_mem hi)⟩
