English
An instance producing a weakly locally compact restricted product when all A_i are open and all but finitely many A_i are compact.
Русский
Инстанс даёт слабую локальную компактность ограниченного произведения, если все A_i открыты и все, кроме конечного числа, A_i компактны.
LaTeX
$$$\\text{WeaklyLocallyCompactSpace}(\\Piʳ i, [R_i, A_i]_{\\text{cofinite}})$ under (∀ i, IsOpen(A_i) ∧ (∀ᶠ i, IsCompact(A_i))).$$
Lean4
instance [hAopen : Fact (∀ i, IsOpen (A i))] [∀ i, WeaklyLocallyCompactSpace (R i)]
[hAcompact : ∀ i, CompactSpace (A i)] : WeaklyLocallyCompactSpace (Πʳ i, [R i, A i]) :=
weaklyLocallyCompactSpace_of_cofinite hAopen.out <| .of_forall fun _ ↦ isCompact_iff_compactSpace.mpr inferInstance
