image — Mathlib

English

For symmetric U, netEntropyInfEntourage T F U ≤ coverEntropyInfEntourage T F U.

Русский

Для симметричной U: netEntropyInfEntourage ≤ coverEntropyInfEntourage.

LaTeX

$$$\operatorname{netEntropyInfEntourage}(T,F,U)\le \operatorname{coverEntropyInfEntourage}(T,F,U)$$$

Lean4

theorem image (h : Semiconj φ S T) {F : Set X} {V : Set (Y × Y)} {n : ℕ} {s : Set X}
    (h' : IsDynCoverOf S F ((map φ φ) ⁻¹' V) n s) : IsDynCoverOf T (φ '' F) V n (φ '' s) :=
  by
  simp only [IsDynCoverOf, image_subset_iff, preimage_iUnion₂, biUnion_image]
  refine h'.trans (iUnion₂_mono fun i _ ↦ subset_of_eq ?_)
  rw [← h.preimage_dynEntourage V n, ball_preimage]

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