isOpen_forall_mem_of_principal — Mathlib

English

If all A_i are open and all but finitely many A_i are compact, then the restricted product with cofinite restriction is weakly locally compact.

Русский

Если все A_i открыты, и все, кроме конечного числа, A_i компактны, то ограниченное произведение с кофинитной ограничением является слабой локально компактной.

LaTeX

$$$\\forall i, IsOpen(A_i) \\;\\land\\; (\\forall^{\\!} i \\text{ in cofinite}, IsCompact(A_i)) \\Rightarrow \\text{WeaklyLocallyCompactSpace}(Πʳ i, [R i, A_i]_{𝓕})$$$

Lean4

theorem isOpen_forall_mem_of_principal {S : Set ι} (hS : cofinite ≤ 𝓟 S) :
    IsOpen {f : Πʳ i, [R i, A i]_[𝓟 S] | ∀ i, f.1 i ∈ A i} :=
  by
  convert isOpen_forall_imp_mem_of_principal hAopen hS (p := fun _ ↦ True)
  simp

Похожие утверждения