coverMincard_finite_of_isCompact_invariant

English

If F is compact and invariant under T (MapsTo T F F), then for any U in the uniformity and n, coverMincard T F U n is strictly below the top.

Русский

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

LaTeX

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

Lean4

theorem coverMincard_finite_of_isCompact_invariant [UniformSpace X] {T : X → X} {F : Set X} (F_comp : IsCompact F)
    (F_inv : MapsTo T F F) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X) (n : ℕ) : coverMincard T F U n < ⊤ :=
  by
  obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_invariant F_comp F_inv U_uni n
  exact s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

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