countable_right_of_prod_of_nonempty

Mathlib.Data.Countable.Basic

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

English

If α is nonempty and α × β is countable, then β is countable.

Русский

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

LaTeX

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

Lean4

theorem countable_right_of_prod_of_nonempty [Nonempty α] (h : Countable (α × β)) : Countable β :=
  by
  contrapose! h
  infer_instance

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

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

Разделы

Аффилиация

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