English
There is a canonical instance asserting that the restricted product is weakly locally compact under the same hypotheses as the principal theorem: each R_i is weakly locally compact, S has cofinite (principal) relation, and each A_i is compact (in its own space).
Русский
Существует канонический экземпляр, утверждающий, что ограниченное произведение является слабой локально компактной, при тех же предпосылках, что и основная теорема: для всех i пространство R_i слабо локально компактно, S имеет ко-конечность, и A_i компактны внутри своих пространств.
LaTeX
$$$\\Bigl(\\forall i,\\; \\text{WeaklyLocallyCompactSpace}(R_i)\\Bigr) \\land (\\text{Fact}(cofinite \\le 𝓟 S)) \\land (\\forall i, \\text{CompactSpace}(A_i)) \\Longrightarrow \\text{WeaklyLocallyCompactSpace}\\left(\\Piʳ i, [R_i, A_i]_{𝓟 S}\\right).$$
Lean4
instance [∀ i, WeaklyLocallyCompactSpace (R i)] [hS : Fact (cofinite ≤ 𝓟 S)] [hAcompact : ∀ i, CompactSpace (A i)] :
WeaklyLocallyCompactSpace (Πʳ i, [R i, A i]_[𝓟 S]) :=
weaklyLocallyCompactSpace_of_principal hS.out fun _ _ ↦ isCompact_iff_compactSpace.mpr inferInstance
