finite_iff

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#Function.Bijective.finite_iff

← MathLib Explorer

English

If f is bijective, then Finite α is equivalent to Finite β.

Русский

Если f биективна, то Finite α ⇄ Finite β.

LaTeX

$$$\\forall {f:\\\\alpha \\\\to \\\\beta}\\ (\\\\text{Bijective}(f)) \\\\Rightarrow \\\\operatorname{Finite}(\\\\alpha) \iff \\\\operatorname{Finite}(\\\\beta).$$$

Lean4

theorem finite_iff {f : α → β} (h : Bijective f) : Finite α ↔ Finite β :=
  (Equiv.ofBijective f h).finite_iff

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

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

Разделы

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

Аффилиация

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