α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ lift (#List e.Γ) ≤ lift ℵ₀
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ (#α) ≤ ℵ₀
refine' Cardinal.lift_le.1 (e.card_le_card_list.trans _)
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ (#List e.Γ) ≤ ℵ₀
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ lift (#List e.Γ) ≤ lift ℵ₀
simp only [Cardinal.lift_aleph0, Cardinal.lift_le_aleph0]
case inl
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
h : IsEmpty e.Γ
⊢ (#List e.Γ) ≤ ℵ₀

case inr
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
h : Nonempty e.Γ
⊢ (#List e.Γ) ≤ ℵ₀
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ (#List e.Γ) ≤ ℵ₀
cases' isEmpty_or_nonempty e.Γ with h h
no goals
case inl
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
h : IsEmpty e.Γ
⊢ (#List e.Γ) ≤ ℵ₀
simp only [Cardinal.mk_le_aleph0]
no goals
case inr
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
h : Nonempty e.Γ
⊢ (#List e.Γ) ≤ ℵ₀
rw [Cardinal.mk_list_eq_aleph0]