English
For any nonempty F, and any n, netMaxcard(T, F, Set.univ, n) = 1.
Русский
Для любого непустого F и любого n справедливо netMaxcard(T, F, Set.univ, n) = 1.
LaTeX
$$$\mathrm{netMaxcard}(T,F,\mathrm{Set.univ},n) = 1.$$$
Lean4
/-- Given an entourage `U` and a time `n`, a dynamical net has a smaller cardinality than
a dynamical cover. This lemma is the first of two key results to compare two versions of
topological entropy: with cover and with nets, the second being `coverMincard_le_netMaxcard`. -/
theorem card_le_card_of_isDynCoverOf {T : X → X} {F : Set X} {U : Set (X × X)} (U_symm : IsSymmetricRel U) {n : ℕ}
{s t : Finset X} (hs : IsDynNetIn T F U n s) (ht : IsDynCoverOf T F U n t) : s.card ≤ t.card :=
by
have (x : X) (x_s : x ∈ s) : ∃ z ∈ t, x ∈ ball z (dynEntourage T U n) :=
by
specialize ht (hs.1 x_s)
simp only [mem_iUnion, exists_prop] at ht
exact ht
choose! F s_t using this
simp only [mem_ball_symmetry (U_symm.dynEntourage T n)] at s_t
apply Finset.card_le_card_of_injOn F fun x x_s ↦ (s_t x x_s).1
exact fun x x_s y y_s Fx_Fy ↦ PairwiseDisjoint.elim_set hs.2 x_s y_s (F x) (s_t x x_s).2 (Fx_Fy ▸ (s_t y y_s).2)
