one_le_netMaxcard_iff

Mathlib.Dynamics.TopologicalEntropy.NetEntropy

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

← MathLib Explorer

English

1 ≤ netMaxcard T F U n iff F is nonempty.

Русский

1 ≤ netMaxcard T F U n эквивалентно не пустоте F.

LaTeX

$$$1 \le netMaxcard(T,F,U,n) \iff F \neq \varnothing.$$$

Lean4

theorem one_le_netMaxcard_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : 1 ≤ netMaxcard T F U n ↔ F.Nonempty :=
  by
  rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty]
  exact not_iff_not.2 (netMaxcard_eq_zero_iff T F U n)

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

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

Разделы

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

Аффилиация

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