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)
:
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)
:
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)
:
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.
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 ⋯