exists_isDynCoverOf_of_isCompact_uniformContinuous

English

If X is a uniform space and F is compact, and T is uniformly continuous, then for any U in the uniformity and n, there exists a finite cover s such that IsDynCoverOf T F U n s.

Русский

При компактности F и непрерывности T существует конечное покрытие s, удовлетворяющее динамическому покрытию с данным U и n.

LaTeX

$$$\exists s, IsDynCoverOf T F U n s$$$

Lean4

theorem exists_isDynCoverOf_of_isCompact_uniformContinuous [UniformSpace X] {T : X → X} {F : Set X}
    (F_comp : IsCompact F) (h : UniformContinuous T) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X) (n : ℕ) :
    ∃ s : Finset X, IsDynCoverOf T F U n s :=
  by
  have uni_ite := dynEntourage_mem_uniformity h U_uni n
  let open_cover := fun x : X ↦ ball x (dynEntourage T U n)
  obtain ⟨s, _, s_cover⟩ := IsCompact.elim_nhds_subcover F_comp open_cover fun (x : X) _ ↦ ball_mem_nhds x uni_ite
  exact ⟨s, s_cover⟩

Похожие утверждения