not_infinite_iff_finite

Mathlib.Data.Finite.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp, push]
theorem not_infinite_iff_finite : ¬Infinite α ↔ Finite α :=
  not_finite_iff_infinite.not_right.symm

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

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

Разделы

Аффилиация

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