Mathlib.Topology.Compactness.LocallyFinite

LocallyFinite.finite_nonempty_inter_compact theorem

{f : ι → Set X} (hf : LocallyFinite f) (hs : IsCompact s) : {i | (f i ∩ s).Nonempty}.Finite

Full source

/-- 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 finite_nonempty_inter_compact {f : ι → Set X}
    (hf : LocallyFinite f) (hs : IsCompact s) : { i | (f i ∩ s).Nonempty }.Finite := by
  choose U hxU hUf using hf
  rcases hs.elim_nhds_subcover U fun x _ => hxU x with ⟨t, -, hsU⟩
  refine (t.finite_toSet.biUnion fun x _ => hUf x).subset ?_
  rintro i ⟨x, hx⟩
  rcases mem_iUnion₂.1 (hsU hx.2) with ⟨c, hct, hcx⟩
  exact mem_biUnion hct ⟨x, hx.1, hcx⟩

Finiteness of Nonempty Intersections between a Locally Finite Family and a Compact Set

Informal description

Let $X$ be a topological space, $s \subseteq X$ a compact set, and $\{f_i\}_{i \in \iota}$ a locally finite family of subsets of $X$. Then the set $\{i \in \iota \mid f_i \cap s \neq \emptyset\}$ is finite.

LocallyFinite.finite_nonempty_of_compact theorem

[CompactSpace X] {f : ι → Set X} (hf : LocallyFinite f) : {i | (f i).Nonempty}.Finite

Full source

/-- If `X` is a compact space, then a locally finite family of sets of `X` can have only finitely
many nonempty elements. -/
theorem finite_nonempty_of_compact [CompactSpace X] {f : ι → Set X}
    (hf : LocallyFinite f) : { i | (f i).Nonempty }.Finite := by
  simpa only [inter_univ] using hf.finite_nonempty_inter_compact isCompact_univ

Finiteness of Nonempty Sets in a Locally Finite Family on a Compact Space

Informal description

Let $X$ be a compact topological space and $\{f_i\}_{i \in \iota}$ a locally finite family of subsets of $X$. Then the set $\{i \in \iota \mid f_i \neq \emptyset\}$ is finite.

LocallyFinite.finite_of_compact theorem

[CompactSpace X] {f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) : (univ : Set ι).Finite

Full source

/-- 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. -/
theorem finite_of_compact [CompactSpace X] {f : ι → Set X}
    (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) : (univ : Set ι).Finite := by
  simpa only [hne] using hf.finite_nonempty_of_compact

Finiteness of Index Set for Locally Finite Family of Nonempty Sets on a Compact Space

Informal description

Let $X$ be a compact topological space and $\{f_i\}_{i \in \iota}$ a locally finite family of nonempty subsets of $X$. Then the index set $\iota$ is finite.

LocallyFinite.fintypeOfCompact definition

[CompactSpace X] {f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) : Fintype ι

Full source

/-- If `X` is a compact space, then a locally finite family of nonempty sets of `X` can have only
finitely many elements, `Fintype` version. -/
noncomputable def fintypeOfCompact [CompactSpace X] {f : ι → Set X}
    (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) : Fintype ι :=
  fintypeOfFiniteUniv (hf.finite_of_compact hne)

Finite type structure for index set of locally finite nonempty family on compact space

Informal description

Let $X$ be a compact topological space and $\{f_i\}_{i \in \iota}$ a locally finite family of nonempty subsets of $X$. Then the index set $\iota$ can be given a finite type structure.