infinite_iff

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.infinite_iff

English

For any equivalence e: α ≃ β, Infinite α ↔ Infinite β.

Русский

Для любой эквиваленции e: α ≃ β, Infinite α ⇔ Infinite β.

LaTeX

$$$\\\\forall e:\\\\alpha \\\\simeq \\\\beta, \\\\operatorname{Infinite}(\\\\alpha) \iff \\\\operatorname{Infinite}(\\\\beta).$$$

Lean4

theorem infinite_iff (e : α ≃ β) : Infinite α ↔ Infinite β :=
  not_finite_iff_infinite.symm.trans <| e.finite_iff.not.trans not_finite_iff_infinite

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

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

Разделы

Аффилиация

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