pi_generateFrom_eq_finite — Mathlib

English

Let X_i be a family of spaces indexed by ι, and for each i a family g(i) of subsets of X_i with ⋃ g(i) = univ. If ι is finite, the product topology on ∏_{i∈ι} X_i is equal to the topology generated by the sets of the form { x ∈ ∏ X_i : x(i) ∈ s_i for all i }, where each s_i ∈ g(i). Equivalently, the topology is generated by sets of the form π_univ s with s ∈ ∏_i g(i).

Русский

Пусть {X_i} задаёт семейство пространств, индексируемое ι, и для каждого i задано семейство g(i) подмножеств X_i так, что ⋃ g(i) = univ. Если ι конечен, топология произведения ∏_{i∈ι} X_i совпадает с топологией, порожденной семейством множеств { x ∈ ∏ X_i : x_i ∈ s_i для всех i }, где каждый s_i ∈ g(i). Эквивалентно, топология равна топологии, порожденной множествами π_univ s, где s ∈ ∀ i, g(i).

LaTeX

$$$\\displaystyle (\\prod_{i:\\iota} X(i))_{\\text{top}} = \\operatorname{generateFrom}\\{ t \\;|\\; \\exists s : \\prod_{i:\\iota} X(i), \\ (\\forall i, s(i) \\in g(i)) \\land t = \\pi_{\\mathrm{univ}} s \\}$$$

Lean4

theorem pi_generateFrom_eq_finite {X : ι → Type*} {g : ∀ a, Set (Set (X a))} [Finite ι] (hg : ∀ a, ⋃₀ g a = univ) :
    (@Pi.topologicalSpace ι X fun a => generateFrom (g a)) =
      generateFrom {t | ∃ s : ∀ a, Set (X a), (∀ a, s a ∈ g a) ∧ t = pi univ s} :=
  by
  cases nonempty_fintype ι
  rw [pi_generateFrom_eq]
  refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)
  · exact fun s ⟨t, ht, Eq⟩ => ⟨t, Finset.univ, by simp [ht, Eq]⟩
  · rintro s ⟨t, i, ht, rfl⟩
    letI := generateFrom {t | ∃ s : ∀ a, Set (X a), (∀ a, s a ∈ g a) ∧ t = pi univ s}
    refine isOpen_iff_forall_mem_open.2 fun f hf => ?_
    choose c hcg hfc using fun a => sUnion_eq_univ_iff.1 (hg a) (f a)
    refine ⟨pi i t ∩ pi ((↑i)ᶜ : Set ι) c, inter_subset_left, ?_, ⟨hf, fun a _ => hfc a⟩⟩
    classical
    rw [← univ_pi_piecewise]
    refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
    by_cases a ∈ i <;> simp [*]

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