# Finiteness of sum types #

source
instance Finite.instSum {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] :
Finite (α ⊕ β)
source
theorem Finite.sum_left {α : Type u_1} (β : Type u_3) [Finite (α ⊕ β)] :
Finite α
source
theorem Finite.sum_right {β : Type u_2} (α : Type u_3) [Finite (α ⊕ β)] :
Finite β
source
instance Finite.instPSum {α : Sort u_3} {β : Sort u_4} [Finite α] [Finite β] :
Finite (α ⊕' β)
source
theorem Finite.psum_left {α : Sort u_3} {β : Sort u_4} [Finite (α ⊕' β)] :
Finite α
source
theorem Finite.psum_right {α : Sort u_3} {β : Sort u_4} [Finite (α ⊕' β)] :
Finite β