isDynNetIn_empty

Mathlib.Dynamics.TopologicalEntropy.NetEntropy

URI: https://scilib.ai/kg/mathlib#Dynamics.isDynNetIn_empty

English

The empty set is always a dynamical net: IsDynNetIn(T,F,U,n,∅) holds for any T, F, U, n.

Русский

Пустое множество всегда образует динамическую сеть: IsDynNetIn(T,F,U,n,∅) выполняется для любых T, F, U, n.

LaTeX

$$IsDynNetIn(T,F,U,n,∅)$$

Lean4

theorem isDynNetIn_empty {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} : IsDynNetIn T F U n ∅ :=
  ⟨empty_subset F, pairwise_empty _⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru