instCountable — Mathlib

English

Let A be a countable set. Then the disjoint union of A with a single new element is countable.

Русский

Пусть A — счётное множество. Тогда дизъюнктное объединение A с одним новым элементом также счётно.

LaTeX

$$$ \operatorname{Countable}(\alpha) \rightarrow \operatorname{Countable}(\alpha \sqcup \{*\}) $$$

Lean4

instance instCountable [Countable α] : Countable (Option α) :=
  Countable.of_equiv _ (Equiv.optionEquivSumPUnit.{0, _} α).symm

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