Compact sets and compact spaces and locally finite functions

theorem LocallyFinite.finite_nonempty_inter_compact {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] {s : Set X} {f : ι → Set X} (hf : LocallyFinite f) (hs : IsCompact s) : {i : ι | (f i ∩ s).Nonempty}.Finite

If s is a compact set in a topological space X and f : ι → Set X is a locally finite family of sets, then f i ∩ s is nonempty only for a finitely many i.

theorem LocallyFinite.finite_nonempty_of_compact {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [CompactSpace X] {f : ι → Set X} (hf : LocallyFinite f) : {i : ι | (f i).Nonempty}.Finite

If X is a compact space, then a locally finite family of sets of X can have only finitely many nonempty elements.

theorem LocallyFinite.finite_of_compact {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [CompactSpace X] {f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ (i : ι), (f i).Nonempty) : Set.univ.Finite

If X is a compact space, then a locally finite family of nonempty sets of X can have only finitely many elements, Set.Finite version.

@[instance_reducible]

noncomputable def LocallyFinite.fintypeOfCompact {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [CompactSpace X] {f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ (i : ι), (f i).Nonempty) : Fintype ι

If X is a compact space, then a locally finite family of nonempty sets of X can have only finitely many elements, Fintype version.

Equations

• hf.fintypeOfCompact hne = Set.fintypeOfFiniteUniv ⋯