English
If the uniformity has a basis, then the entropy equals the corresponding supremum over basis elements; i.e., coverEntropy T F equals the supremum over i of coverEntropyEntourage T F (s i) with the appropriate indices.
Русский
Если униформность имеет базис, энтропия равна соответствующему супремуму по базисным элементам: coverEntropy T F = sup_i coverEntropyEntourage T F (s i).
LaTeX
$$$\operatorname{coverEntropy}(T,F) = \sup_{i} \operatorname{coverEntropyEntourage}(T,F,s(i))$$$
Lean4
theorem coverEntropy_eq_iSup_basis {ι : Sort*} {p : ι → Prop} {s : ι → Set (X × X)} (h : (𝓤 X).HasBasis p s) (T : X → X)
(F : Set X) : coverEntropy T F = ⨆ (i : ι) (_ : p i), coverEntropyEntourage T F (s i) :=
by
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)
obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
exact
(coverEntropyEntourage_antitone T F si_U).trans
(le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyEntourage T F (s i)) i h_i)
