ofBijective

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#Finite.ofBijective

← MathLib Explorer

English

If α is finite and f: α → β is bijective, then β is finite.

Русский

Если α конечна и f: α → β биективна, тогда β конечна.

LaTeX

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

Lean4

theorem ofBijective [Finite α] {f : α → β} (h : Bijective f) : Finite β :=
  h.finite_iff.mp ‹_›

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

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

Разделы

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

Аффилиация

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