English
If X is sigma-compact, then any locally finite family f: ι → Set X of nonempty subsets has a countable index set; i.e., univ in ι is countable.
Русский
Если X σ-компактно, то любая локально конечная family f: ι → Set X из непустых подмножеств имеет счетный индексный набор; то есть множество индексов ι счетно.
LaTeX
$$$$\text{LocallyFinite}(f) \Rightarrow (univ : Set\ ι).Countable,$$ при условии $\forall i, (f(i)).Nonempty$ и $[\SigmaCompactSpace X].$$$
Lean4
/-- If `X` is a `σ`-compact space, then a locally finite family of nonempty sets of `X` can have
only countably many elements, `Set.Countable` version. -/
protected theorem countable_univ {f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) :
(univ : Set ι).Countable :=
by
have := fun n => hf.finite_nonempty_inter_compact (isCompact_compactCovering X n)
refine (countable_iUnion fun n => (this n).countable).mono fun i _ => ?_
rcases hne i with ⟨x, hx⟩
rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering X) x with ⟨n, hn⟩
exact mem_iUnion.2 ⟨n, x, hx, hn⟩
