English
If F is nonempty, then netEntropyEntourage T F U ≥ 0.
Русский
Если F непусто, то netEntropyEntourage T F U ≥ 0.
LaTeX
$$$F\neq\emptyset\Rightarrow 0\le \operatorname{netEntropyEntourage}(T,F,U)$$$
Lean4
theorem coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage {ι : Sort*} {p : ι → Prop} {s : ι → Set (X × X)}
(h : (𝓤 X).HasBasis p s) (T : X → X) (F : Set X) :
coverEntropyInf T F = ⨆ (i : ι) (_ : p i), netEntropyInfEntourage T F (s i) :=
by
rw [coverEntropyInf_eq_iSup_netEntropyInfEntourage T F]
apply (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩).antisymm'
refine iSup₂_le fun U U_uni ↦ ?_
obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
apply (netEntropyInfEntourage_antitone T F si_U).trans
exact le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ netEntropyInfEntourage T F (s i)) i h_i