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