Theorems · Definition · combinatorics

Fintype.sumRight

{α : Type u_4} → {β : Type u_5} → [Fintype (α ⊕ β)] → Fintype β

Given that α ⊕ β is a fintype, β is also a fintype. This is non-computable as it uses that Sum.inr is an injection, but there's no clear inverse if β is empty.

Defined in

Mathlib.Data.Fintype.Card

Cited by

0 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype