of_not_small

Mathlib.Data.Countable.Small

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

English

If a type is not small, then it is uncountable.

Русский

Если тип не мал, то он несчётен.

LaTeX

$$$\\lnot Small(\\alpha) \\rightarrow Uncountable(\\alpha)$$$

Lean4

theorem of_not_small {α : Type v} (h : ¬Small.{w} α) : Uncountable α :=
  by
  rw [uncountable_iff_not_countable]
  exact mt (@Countable.toSmall α) h

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

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

Разделы

Аффилиация

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