coverEntropyInfEntourage_le_coverEntropyInf

English

If the uniformity is generated by a basis {s_i} with p_i, then coverEntropyInf T F equals the supremum over i of coverEntropyInfEntourage T F (s_i).

Русский

Если униформность задаётся базисом {s_i} с условиями p_i, то coverEntropyInf T F равноSupremum по i: coverEntropyInfEntourage T F (s_i).

LaTeX

$$$\text{If } (\mathcal{U}X).HasBasis(p,s),\; \operatorname{coverEntropyInf}(T,F) = \bigvee_{i} p(i) \; \operatorname{coverEntropyInfEntourage}(T,F,s(i)).$$$

Lean4

theorem coverEntropyInfEntourage_le_coverEntropyInf (T : X → X) (F : Set X) {U : Set (X × X)} (h : U ∈ 𝓤 X) :
    coverEntropyInfEntourage T F U ≤ coverEntropyInf T F :=
  le_iSup₂ (f := fun (U : Set (X × X)) (_ : U ∈ 𝓤 X) ↦ coverEntropyInfEntourage T F U) U h

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