coverEntropy_eq_iSup_basis_netEntropyEntourage

English

As above, 0 ≤ netEntropyEntourage T F U when F is nonempty.

Русский

Как выше, если F непусто, то 0 ≤ netEntropyEntourage T F U.

LaTeX

$$$F\neq\emptyset\Rightarrow 0\le \operatorname{netEntropyEntourage}(T,F,U)$$$

Lean4

theorem coverEntropy_eq_iSup_basis_netEntropyEntourage {ι : Sort*} {p : ι → Prop} {s : ι → Set (X × X)}
    (h : (𝓤 X).HasBasis p s) (T : X → X) (F : Set X) :
    coverEntropy T F = ⨆ (i : ι) (_ : p i), netEntropyEntourage T F (s i) :=
  by
  rw [coverEntropy_eq_iSup_netEntropyEntourage 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 (netEntropyEntourage_antitone T F si_U).trans _
  exact le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ netEntropyEntourage T F (s i)) i h_i

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