subset_countable_closure_of_compact

English

A compact set s has a subset t ⊆ s which is countable and such that s ⊆ closure t.

Русский

Компактное множество s содержит счетное подмножество t ⊆ s, чьё замыкание покрывает s.

LaTeX

$$∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t$$

Lean4

/-- A compact set in a pseudo emetric space is separable, i.e., it is a subset of the closure of a
countable set. -/
theorem subset_countable_closure_of_compact {s : Set α} (hs : IsCompact s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t :=
  by
  refine subset_countable_closure_of_almost_dense_set s fun ε hε => ?_
  rcases totallyBounded_iff'.1 hs.totallyBounded ε hε with ⟨t, -, htf, hst⟩
  exact ⟨t, htf.countable, hst.trans <| iUnion₂_mono fun _ _ => ball_subset_closedBall⟩

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