Compactness utilities

General lemmas about compact and σ-compact subsets of topological spaces, and limits along ultrafilters of families eventually in a compact set.

theorem IsCompact.inter_of_forall_exists {X : Type u_1} [TopologicalSpace X] {U S : Set X} (hU : IsCompact U) (h : ∀ x ∈ U, ∃ U' ⊆ U, IsOpen U' ∧ x ∈ U' ∧ IsCompact (U' ∩ S)) : IsCompact (U ∩ S)

Compactness of U ∩ S for a compact set U may be checked on open pieces of U around each of its points.

theorem IsCompact.connectedComponentIn {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (x : X) : IsCompact (connectedComponentIn K x)

Connected components of a compact set are compact. The connected component of a compact set K at a point is closed in K, hence compact; it is empty at a point outside K.

theorem IsCompact.image_connectedComponentIn {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] {K A : Set X} {f : X → Y} (hK : IsCompact K) (hf : ContinuousOn f K) (hinj : Set.InjOn f K) (hA : A ⊆ K) {x : X} (hx : x ∈ K) : f '' connectedComponentIn A x = connectedComponentIn (f '' A) (f x)

A continuous injection on a compact set maps components onto components. If f is continuous and injective on a compact set K with values in a Hausdorff space, and A ⊆ K, then f maps the connected component of A at a point x ∈ K onto the connected component of f '' A at f x. Both sides are empty when x ∉ A.

theorem IsCompact.exists_tendsto_of_eventually_mem {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {s : Set X} (hs : IsCompact s) {U : Ultrafilter ι} {u : ι → X} (hu : ∀ᶠ (i : ι) in ↑U, u i ∈ s) : ∃ x ∈ s, Filter.Tendsto u (↑U) (nhds x)

A family that eventually lies in a compact set s along an ultrafilter converges along it to a point of s.

theorem TauCeti.not_isCompact_connectedComponent {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] [NoncompactSpace X] (x : X) : ¬IsCompact (connectedComponent x)

A preconnected noncompact space has no compact connected component: its only component is the whole space.

theorem TauCeti.isCompact_closure_connectedComponentIn_compl_of_mem {X : Type u_1} [TopologicalSpace X] {S : Set X} {x : X} (hx : x ∈ S) : IsCompact (closure (connectedComponentIn Sᶜ x))

The component in Sᶜ of a point of S is empty, so its closure is compact.

theorem TauCeti.notMem_of_not_isCompact_closure_connectedComponentIn_compl {X : Type u_1} [TopologicalSpace X] {S : Set X} {x : X} (hx : ¬IsCompact (closure (connectedComponentIn Sᶜ x))) : x ∉ S

A point whose component in Sᶜ has noncompact closure lies outside S.

theorem IsSigmaCompact.union {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hs : IsSigmaCompact s) (ht : IsSigmaCompact t) : IsSigmaCompact (s ∪ t)

The union of two σ-compact sets is σ-compact.

theorem TauCeti.isCompact_inter_preimage_comp_prodMk_left {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] [T1Space Z] {s : Set X} {I : Set Z} {H : X × Z → Y} {U : Set Y} (hHp : ∀ (K : Set Y), IsCompact K → K ⊆ U → IsCompact (s ×ˢ I ∩ H ⁻¹' K)) {t : Z} (ht : t ∈ I) (K : Set Y) (hK : IsCompact K) (hKU : K ⊆ U) : IsCompact (s ∩ (fun (x : X) => H (x, t)) ⁻¹' K)

Slices of a map proper on s ×ˢ I are proper: if (s ×ˢ I) ∩ H ⁻¹' K is compact for every compact K ⊆ U, then so is s ∩ H (·, t) ⁻¹' K for every t ∈ I.

theorem IsCompact.finite_of_forall_isClosed {X : Type u_1} [TopologicalSpace X] {K S : Set X} (hK : IsCompact K) (hSK : S ⊆ K) (hS : ∀ T ⊆ S, IsClosed T) : S.Finite

A compact set contains no infinite subset all of whose subsets are closed: such a subset would be closed, hence compact, and discrete.

theorem TauCeti.isOpen_forall_prodMk_mem {α : Type u_2} {E : Type u_3} {P : Type u_4} [TopologicalSpace α] [CompactSpace α] [TopologicalSpace E] [TopologicalSpace P] {ι : α → P} {W : Set (E × P)} (hι : Continuous ι) (hW : IsOpen W) : IsOpen {x : E | ∀ (y : α), (x, ι y) ∈ W}

If W is open and ι is continuous on a compact space, the set of parameters x with {x} × ι(α) ⊆ W is open.