dense_pi — Mathlib

English

If each s_i is dense in X_i for i ∈ I, then pi I s is dense in the product space.

Русский

Если для всех i ∈ I множества s_i плотно заполнены в X_i, то их произведение плотны в произведении пространств.

LaTeX

$$$$ (\\\\forall i \\in I, \\overline{s_i} = X_i) \\\\Rightarrow \\\\overline{\\\\pi I s} = \\\\prod_i X_i. $$$$

Lean4

theorem dense_pi {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {s : ∀ i, Set (α i)} (I : Set ι)
    (hs : ∀ i ∈ I, Dense (s i)) : Dense (pi I s) := by
  simp only [dense_iff_closure_eq, closure_pi_set, pi_congr rfl fun i hi => (hs i hi).closure_eq, pi_univ]

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