English
For any T and F, the map assigning to each uniformity u the quantity coverEntropyInf(T, F) is antitone with respect to refinement of entourages; i.e., if U ⊆ V then coverEntropyInfEntourage(T, F, U) ≥ coverEntropyInfEntourage(T, F, V).
Русский
Для любых T и F отображение, ставящее в соответствие энтропию по окружению, является антитоническим по отношению к уточнению окрестностей: если U ⊆ V, то coverEntropyInfEntourage(T, F, U) ≥ coverEntropyInfEntourage(T, F, V).
LaTeX
$$$\text{Antitone }(u \mapsto \operatorname{coverEntropyInfEntourage}(T,F,u))$; in particular, if $U \subseteq V$ then $\operatorname{coverEntropyInfEntourage}(T,F,U) \ge \operatorname{coverEntropyInfEntourage}(T,F,V)$.$$
Lean4
theorem coverEntropyInf_antitone (T : X → X) (F : Set X) :
Antitone fun (u : UniformSpace X) ↦ @coverEntropyInf X u T F := fun _ _ h ↦
iSup₂_mono' fun U U_uni ↦ ⟨U, (le_def.1 h) U U_uni, le_refl _⟩
