English
If s is a minimal dynamical cover of F by U at level n, and its size equals the minimal cover card, then every x in s has a nonempty intersection F ∩ ball(x, dynEntourage T U n).
Русский
Пусть s — минимальное динамическое покрытие F по U на уровне n; тогда пересечение каждого ball(x, dynEntourage(T,U,n)) с F непусто для каждого x ∈ s.
LaTeX
$$IsDynCoverOf T F U n s → s.card = coverMincard T F U n → ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty$$
Lean4
/-- All dynamical balls of a minimal dynamical cover of `F` intersect `F`. This lemma is the key
to relate Bowen-Dinaburg's definition of topological entropy with covers and their definition
of topological entropy with nets. -/
theorem nonempty_inter_of_coverMincard {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} {s : Finset X}
(h : IsDynCoverOf T F U n s) (h' : s.card = coverMincard T F U n) :
∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty := by
-- Otherwise, there is a ball which does not intersect `F`. Removing it yields a smaller cover.
classical
by_contra! hypo
obtain ⟨x, x_s, ball_empt⟩ := hypo
have smaller_cover : IsDynCoverOf T F U n (s.erase x) :=
by
intro y y_F
specialize h y_F
simp only [s.mem_coe, mem_iUnion, exists_prop] at h
simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff, mem_iUnion, exists_prop]
obtain ⟨z, z_s, hz⟩ := h
refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
rw [← ball_empt]
rw [z_x] at hz
exact mem_inter y_F hz
apply smaller_cover.coverMincard_le_card.not_gt
rw [← h']
exact_mod_cast s.card_erase_lt_of_mem x_s
