coverEntropy_biUnion_finset — Mathlib

English

For a finite set s of indices, coverEntropy T (⋃ i ∈ s, F i) equals the supremum over i ∈ s of coverEntropy T (F i).

Русский

Для конечного множества индексов s энтропия покрытия равна наибольшему значению энтропии покрытий F_i для i ∈ s.

LaTeX

$$$\\operatorname{coverEntropy} T\\left(\\bigcup_{i\\in s} F_i\\right) = \\bigvee_{i\\in s} \\operatorname{coverEntropy} T(F_i)$$$

Lean4

theorem coverEntropy_biUnion_finset {T : X → X} {F : ι → Set X} {s : Finset ι} :
    coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i) :=
  by
  have := map_finset_sup (coverEntropy_supBotHom T) s F
  rw [s.sup_set_eq_biUnion, s.sup_eq_iSup, coverEntropy_supBotHom, SupBotHom.coe_mk, SupHom.coe_mk] at this
  rw [this]
  congr

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