instFintypeSum — Mathlib

English

The disjoint sum α ⊕ β is finite whenever α and β are finite; a natural enumeration is univ.disjSum univ.

Русский

Дисъюнктное объединение α ⊕ β конечно, если α и β конечно; естественное перечисление — univ.disjSum univ.

LaTeX

$$$Fintype(\alpha \oplus \beta)$$$

Lean4

instance (α : Type u) (β : Type v) [Fintype α] [Fintype β] : Fintype (α ⊕ β)
    where
  elems := univ.disjSum univ
  complete := by rintro (_ | _) <;> simp

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