English
Analogously, coverEntropyInf T F equals the supremum over i of coverEntropyInfEntourage T F (s i) when a basis exists for the uniformity.
Русский
Аналогично, если существует база униформности, то coverEntropyInf T F равно sup_i coverEntropyInfEntourage T F (s i).
LaTeX
$$$\operatorname{coverEntropyInf}(T,F) = \sup_{i} \operatorname{coverEntropyInfEntourage}(T,F,s(i)).$$$
Lean4
theorem coverEntropyInf_eq_iSup_basis {ι : Sort*} {p : ι → Prop} {s : ι → Set (X × X)} (h : (𝓤 X).HasBasis p s)
(T : X → X) (F : Set X) : coverEntropyInf T F = ⨆ (i : ι) (_ : p i), coverEntropyInfEntourage 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
(coverEntropyInfEntourage_antitone T F si_U).trans
(le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyInfEntourage T F (s i)) i h_i)
