countable_infinite_iff_nonempty_denumerable

English

A subset s is countable and infinite if and only if s is denumerable.

Русский

Подмножество s счётно и бесконечно тогда и только тогда, когда оно денумерабельно.

LaTeX

$$$ s.Countable \wedge s.Infinite \iff Nonempty(\text{Denumerable}(s)) $$$

Lean4

theorem _root_.Set.countable_infinite_iff_nonempty_denumerable {α : Type*} {s : Set α} :
    s.Countable ∧ s.Infinite ↔ Nonempty (Denumerable s) := by
  rw [nonempty_denumerable_iff, ← Set.infinite_coe_iff, countable_coe_iff]

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