of_equiv

Mathlib.Data.Countable.Defs

URI: https://scilib.ai/kg/mathlib#Uncountable.of_equiv

English

If α is uncountable and e : α ≃ β is a bijection, then β is uncountable.

Русский

Пусть α несчётно, и существует биекция e : α ≃ β; тогда β несчётно.

LaTeX

$$$Uncountable(\\alpha) \\rightarrow (\\alpha \\cong \\beta) \\rightarrow Uncountable(\\beta)$$$

Lean4

theorem of_equiv (α : Sort*) [Uncountable α] (e : α ≃ β) : Uncountable β :=
  e.injective.uncountable

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

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

Разделы

Аффилиация

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