The pairs of natural numbers with bounded sum

The pairs (i, j) of natural numbers with i + j < m are the union of the antidiagonals i + j = s for s < m, and there are m (m + 1) / 2 of them.

Main results

• Finset.Nat.two_mul_card_biUnion_range_antidiagonal: the union of the antidiagonals i + j = s for s < m has m (m + 1) / 2 elements.

theorem Finset.Nat.two_mul_card_biUnion_range_antidiagonal (m : ℕ) : 2 * ((range m).biUnion antidiagonal).card = m * (m + 1)

There are m (m + 1) / 2 pairs of natural numbers with sum less than m: the union of the antidiagonals i + j = s for s < m has m (m + 1) / 2 elements.