not_finite_iff_infinite

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#not_finite_iff_infinite

English

For any α, not Finite α is equivalent to Infinite α.

Русский

Для любого α, Not Finite α эквивалентно Infinite α.

LaTeX

$$$\\neg\\operatorname{Finite}(\\alpha) \\iff \\operatorname{Infinite}(\\alpha).$$$

Lean4

@[simp, push]
theorem not_finite_iff_infinite : ¬Finite α ↔ Infinite α :=
  ⟨Infinite.mk, fun h => h.1⟩

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

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

Разделы

Аффилиация

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