countable_iff — Mathlib

English

For any equivalence e: α ≃ β, α is countable if and only if β is countable.

Русский

Для любого эквивалентного отображения e: α ≃ β, счётность α эквивалентна счётности β.

LaTeX

$$$\forall e:\alpha\simeq\beta,\ \operatorname{Countable}(\alpha) \iff \operatorname{Countable}(\beta)$$$

Lean4

theorem countable_iff (e : α ≃ β) : Countable α ↔ Countable β :=
  ⟨fun h => @Countable.of_equiv _ _ h e, fun h => @Countable.of_equiv _ _ h e.symm⟩

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