isCompact_closure_iff — Mathlib

English

In a family of spaces indexed by i, closure_iff equivalence holds: compact closures can be checked componentwise.

Русский

Во множестве пространства, индексированного i, замыкание можно проверить компонентно через компакты каждого i.

LaTeX

$$$IsCompact (closure s) \\iff \\forall i, IsCompact (closure (eval_i '' s)).$$$

Lean4

theorem isCompact_closure_iff {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T2Space (X i)]
    {s : Set (Π i, X i)} : IsCompact (closure s) ↔ ∀ i, IsCompact (closure <| eval i '' s) := by
  simp_rw [← exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, image_subset_iff]

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