coverMincard_finite_of_isCompact_uniformContinuous

English

If F is compact and T is uniformly continuous, then for any U in the uniformity and any n, coverMincard T F U n is finite (strictly below top).

Русский

Если F компактно, а T равномерно непрерывна, то для любого U из Uniformity и любого n покрытие имеет конечную минимальную карту.

LaTeX

$$IsCompact F → UniformContinuous T → (∀ {U}, U ∈ 𝒰 X → ∀ n, coverMincard T F U n < ⊤)$$

Lean4

theorem coverMincard_finite_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 : ℕ) :
    coverMincard T F U n < ⊤ :=
  by
  obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_uniformContinuous F_comp h U_uni n
  exact s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

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