English
If the index set ι is finite and each X_i is locally compact, then the product space ∀ i, X_i is locally compact.
Русский
Если индексный множитель ι конечен и каждый X_i локально компактен, то произведение по индексу локально компактно.
LaTeX
$$$[Finite\;\iota] \Rightarrow LocallyCompactSpace\; (\forall i:\iota, X_i)$$$
Lean4
/-- In general it suffices that all but finitely many of the spaces are compact,
but that's not straightforward to state and use. -/
instance locallyCompactSpace_of_finite [Finite ι] : LocallyCompactSpace (∀ i, X i) :=
⟨fun t n hn => by
rw [nhds_pi, Filter.mem_pi] at hn
obtain ⟨s, -, n', hn', hsub⟩ := hn
choose n'' hn'' hsub' hc using fun i => LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)
refine ⟨(Set.univ : Set ι).pi n'', ?_, subset_trans (fun _ h => ?_) hsub, isCompact_univ_pi hc⟩
· exact (set_pi_mem_nhds_iff (@Set.finite_univ ι _) _).mpr fun i _ => hn'' i
· exact fun i _ => hsub' i (h i trivial)⟩
