isDynNetIn_singleton

Mathlib.Dynamics.TopologicalEntropy.NetEntropy

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

← MathLib Explorer

English

A singleton {x} is a dynamical net provided x ∈ F: IsDynNetIn(T,F,U,n,{x}).

Русский

Один элемент {x} образует динамическую сеть при условии x ∈ F: IsDynNetIn(T,F,U,n,{x}).

LaTeX

$$IsDynNetIn(T,F,U,n,{x})$$

Lean4

theorem isDynNetIn_singleton (T : X → X) {F : Set X} (U : Set (X × X)) (n : ℕ) {x : X} (h : x ∈ F) :
    IsDynNetIn T F U n { x } :=
  ⟨singleton_subset_iff.2 h, pairwise_singleton x _⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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