English
If for every index i the space R_i is weakly locally compact, S has finite complement in I, and A_i is compact for all i ∈ S, then the restricted product Πʳ_i [R_i, A_i]_{𝓟 S} is weakly locally compact.
Русский
Пусть для каждого индекса i пространство R_i является слабо локально компактным, множество S имеет конечное дополнение к ι, и A_i компактно для всех i ∈ S. Тогда ограниченное произведение Πʳ_i [R_i, A_i]_{𝓟 S} является слабой локально компактной пространством.
LaTeX
$$$\\Bigl(\\forall i,\\; \\text{WeaklyLocallyCompactSpace}(R_i)\\Bigr) \\land (cofinite \\le 𝓟 S) \\land \\Bigl(\\forall i \\in S, \\text{IsCompact}(A_i)\\Bigr) \\Longrightarrow \\text{WeaklyLocallyCompactSpace}\\left(\\Piʳ i, [R_i, A_i]_{𝓟 S}\\right).$$
Lean4
/-- Assume that `S` is a subset of `ι` with finite complement, that each `R i` is weakly locally
compact, and that `A i` is *compact* for all `i ∈ S`. Then the restricted product
`Πʳ i, [R i, A i]_[𝓟 S]` is locally compact.
Note: we spell "`S` has finite complement" as `cofinite ≤ 𝓟 S`. -/
theorem weaklyLocallyCompactSpace_of_principal [∀ i, WeaklyLocallyCompactSpace (R i)] (hS : cofinite ≤ 𝓟 S)
(hAcompact : ∀ i ∈ S, IsCompact (A i)) : WeaklyLocallyCompactSpace (Πʳ i, [R i, A i]_[𝓟 S]) where
exists_compact_mem_nhds := fun x ↦ by
rw [le_principal_iff, mem_cofinite] at hS
classical
have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
choose K K_compact hK using this
set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def
have Q_compact : IsCompact Q :=
isCompact_univ_pi fun i ↦ by
split_ifs with his
· exact hAcompact i his
· exact K_compact i
set U : Set (Π i, R i) := Sᶜ.pi K
have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
have QU : (↑) ⁻¹' U ⊆ ((↑) ⁻¹' Q : Set (Πʳ i, [R i, A i]_[𝓟 S])) := fun y H i _ ↦
by
dsimp only
split_ifs with hi
· exact y.2 hi
· exact H i hi
refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
· refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]
exact inter_subset_left
· simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds
