sumLeft — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Given that `α ⊕ β` is a fintype, `α` is also a fintype. This is non-computable as it uses
that `Sum.inl` is an injection, but there's no clear inverse if `α` is empty. -/
noncomputable def sumLeft {α β} [Fintype (α ⊕ β)] : Fintype α :=
  Fintype.ofInjective (Sum.inl : α → α ⊕ β) Sum.inl_injective

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