α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : Nonempty α
s : Set α
h : Set.Countable s
inhabited_h : Inhabited α
⊢ ∃ f, s ⊆ range f
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : Nonempty α
s : Set α
h : Set.Countable s
⊢ ∃ f, s ⊆ range f
inhabit α
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : Nonempty α
s : Set α
h : Set.Countable s
inhabited_h : Inhabited α
⊢ ∃ f, s ⊆ range f
exact ⟨enumerateCountable h default, subset_range_enumerate _ _⟩