isCompact_closure_interUnionBalls

English

Under a HasBasis for the uniformity and [CompleteSpace α], the closure of interUnionBalls is compact.

Русский

При наличии основы равномерности и полного пространства α замыкание interUnionBalls компактно.

LaTeX

$$$IsCompact(\overline{\operatorname{interUnionBalls}(xs,u,U)})$$$

Lean4

/-- The construction `interUnionBalls` is used to have a relatively compact set. -/
theorem isCompact_closure_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)} (H : (uniformity α).HasBasis p U)
    [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) : IsCompact (closure (interUnionBalls xs u U)) :=
  by
  rw [isCompact_iff_totallyBounded_isComplete]
  refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
  exact totallyBounded_interUnionBalls H xs u

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