closure_pi_set — Mathlib

English

Closure distributes over pi: closure(pi I s) = pi I (closure(s_i)).

Русский

Замыкание распределяется над произведением: closure(pi I s) = pi I closure(s_i).

LaTeX

$$$$ closure(\\\\pi I s) = \\\\pi I (\\\\lambda i, closure(s_i)). $$$$

Lean4

theorem closure_pi_set {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] (I : Set ι) (s : ∀ i, Set (α i)) :
    closure (pi I s) = pi I fun i => closure (s i) :=
  Set.ext fun _ => mem_closure_pi

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