coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage

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

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