instFiniteElemProdNatPreimageHAddFstSndSingletonSet

English

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

Русский

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

LaTeX

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

Lean4

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

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