sumRight — Mathlib

English

If α ⊕ β is finite, then β is finite.

Русский

Если α ⊕ β конечна, то β конечна.

LaTeX

$$$ \mathrm{Fintype}(\alpha \oplus \beta) \Rightarrow \mathrm{Fintype}(\beta) $$$

Lean4

/-- 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. -/
noncomputable def sumRight {α β} [Fintype (α ⊕ β)] : Fintype β :=
  Fintype.ofInjective (Sum.inr : β → α ⊕ β) Sum.inr_injective

Похожие утверждения