instUncountableProdOfNonempty_1

Mathlib.Data.Countable.Basic

URI: https://scilib.ai/kg/mathlib#instUncountableProdOfNonempty_1

English

If a is nonempty and β is uncountable, then α × β is uncountable.

Русский

Если α непусто, а β несчётно, то α × β несчётно.

LaTeX

$$$ \operatorname{Nonempty}(\alpha) \land \operatorname{Uncountable}(\beta) \rightarrow \operatorname{Uncountable}(\alpha \times \beta) $$$

Lean4

instance [Nonempty α] [Uncountable β] : Uncountable (α × β) :=
  by
  inhabit α
  exact (Prod.mk_right_injective default).uncountable

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

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

Разделы

Аффилиация

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