class PiBase.CountablyInfinite (X : Type u_1) extends Countable X, Infinite X : Prop

181. Countably infinite

• exists_injective_nat' : ∃ (f : X → ℕ), Function.Injective f
• not_finite : ¬Finite X