mem_closure_pi — Mathlib

English

x ∈ closure of product pi-s is equivalent to each coordinate x_i ∈ closure of s_i on I.

Русский

Точка x принадлежит замыканию произведения π I s тогда и только тогда, когда для каждой координаты x_i принадлежит замыканию s_i.

LaTeX

$$$$ x \\in closure(\\\\pi I s) \\\\iff \\\\forall i \\in I, x_i \\in closure(s_i). $$$$

Lean4

theorem mem_closure_pi {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {I : Set ι} {s : ∀ i, Set (α i)}
    {x : ∀ i, α i} : x ∈ closure (pi I s) ↔ ∀ i ∈ I, x i ∈ closure (s i) := by
  simp only [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_pi_neBot]

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