English
The entropy for the empty cover with any F is bottom: netEntropyInfEntourage T Set.empty U = ⊥.
Русский
Энтропия для пустого множества покрытий равна нижней границе: netEntropyInfEntourage T пустой F = ⊥.
LaTeX
$$$\operatorname{netEntropyInfEntourage}(T,\emptyset,U)=\bot$$$
Lean4
/-- Bowen-Dinaburg's definition of topological entropy using nets is
`⨆ U ∈ 𝓤 X, netEntropyEntourage T F U`. This quantity is the same as the topological entropy using
covers, so there is no need to define a new notion of topological entropy. This version of the
theorem relates the `limsup` versions of topological entropy. -/
theorem coverEntropy_eq_iSup_netEntropyEntourage : coverEntropy T F = ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U :=
by
apply le_antisymm <;> refine iSup₂_le fun U U_uni ↦ ?_
· obtain ⟨V, V_uni, V_symm, V_comp_U⟩ := comp_symm_mem_uniformity_sets U_uni
apply (coverEntropyEntourage_antitone T F V_comp_U).trans (le_iSup₂_of_le V V_uni _)
exact coverEntropyEntourage_le_netEntropyEntourage T F (refl_le_uniformity V_uni) V_symm
· apply (netEntropyEntourage_antitone T F (symmetrizeRel_subset_self U)).trans
apply (le_iSup₂ (symmetrizeRel U) (symmetrize_mem_uniformity U_uni)).trans'
exact netEntropyEntourage_le_coverEntropyEntourage T F (symmetric_symmetrizeRel U)
