English
If each f i has a basis with index set p and cylinder s i, then hasBasis for pi f with combined index.
Русский
Если каждый f i имеет базис с индексом p и цилиндр s i, тогда для pi f получается общий базис.
LaTeX
$$$\forall I, k, ..., (hasBasis) \Rightarrow (pi f) HasBasis (...).$$$
Lean4
theorem hasBasis_pi_same_index {κ : Type*} {p : κ → Prop} {s : Π i : ι, κ → Set (α i)}
(h : ∀ i : ι, (f i).HasBasis p (s i))
(h_dir : ∀ I : Set ι, ∀ k : ι → κ, I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)) :
(pi f).HasBasis (fun Ik : Set ι × κ ↦ Ik.1.Finite ∧ p Ik.2) (fun Ik ↦ Ik.1.pi (fun i ↦ s i Ik.2)) :=
by
refine hasBasis_pi h |>.to_hasBasis ?_ ?_
· rintro ⟨I, k⟩ ⟨hI, hk⟩
rcases h_dir I k hI hk with ⟨k₀, hk₀, hk₀'⟩
exact ⟨⟨I, k₀⟩, ⟨hI, hk₀⟩, Set.pi_mono hk₀'⟩
· rintro ⟨I, k⟩ ⟨hI, hk⟩
exact ⟨⟨I, fun _ ↦ k⟩, ⟨hI, fun _ _ ↦ hk⟩, subset_rfl⟩
