instFiniteElemProdNatSetOfEqHAddFstSnd

English

For every natural number n, the set of triples (i1,i2,i3) of natural numbers with i1+i2+i3 = n is finite.

Русский

Для каждого натурального числа n множество троек (i1,i2,i3) таких, что i1+i2+i3 = n, конечное.

LaTeX

$$$\#\{(i_1,i_2,i_3) \in \mathbb{N}^3 \mid i_1+i_2+i_3=n\} < \infty$$$

Lean4

instance (n : ℕ) : Finite ({i : (ℕ × ℕ × ℕ) | i.1 + i.2.1 + i.2.2 = n}) :=
  by
  refine
    Finite.of_injective
      (fun ⟨⟨i₁, i₂, i₃⟩, (hi : i₁ + i₂ + i₃ = n)⟩ =>
        (⟨⟨i₁, by cutsat⟩, ⟨i₂, by cutsat⟩, ⟨i₃, by cutsat⟩⟩ : Fin (n + 1) × Fin (n + 1) × Fin (n + 1)))
      ?_
  rintro ⟨⟨_, _, _⟩, _⟩ ⟨⟨_, _, _⟩, _⟩ h
  simpa using h

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