finite_of_discrete — Mathlib

English

Let X have the discrete topology. If s is compact, then s is finite.

Русский

Пусть X имеет дискретную топологию. Тогда если s компактно, то s конечно.

LaTeX

$$$\text{DiscreteTopology}(X) \Rightarrow (\operatorname{IsCompact}(s) \Rightarrow \#s < \infty)$$$

Lean4

theorem finite_of_discrete [DiscreteTopology X] (hs : IsCompact s) : s.Finite :=
  by
  have : ∀ x : X, ({ x } : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
  rcases hs.elim_nhds_subcover (fun x => { x }) fun x _ => this x with ⟨t, _, hst⟩
  simp only [← t.set_biUnion_coe, biUnion_of_singleton] at hst
  exact t.finite_toSet.subset hst

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