English
There exists a canonical equivalence between the totalization of divisorsAntidiagonal and product of positive naturals; inverse respects fst and snd projections as shown by lemmas.
Русский
Существует каноническая эквивалентность между суммаризацией divisorsAntidiagonal и произведением положительных натуральных чисел; её обратное отображение сохраняет проекции fst и snd как показано леммами.
LaTeX
$$$$ \text{equiv} : ((\Sigma n : \mathbb{N}^+, Nat.divisorsAntidiagonal n)) \simeq \mathbb{N}_+ \times \mathbb{N}_+ $$$$
Lean4
/-- The equivalence from the union over `n` of `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+`
given by sending `n = a * b` to `(a, b)`. -/
def sigmaAntidiagonalEquivProd : (Σ n : ℕ+, Nat.divisorsAntidiagonal n) ≃ ℕ+ × ℕ+
where
toFun x := divisorsAntidiagonalFactors x.1 x.2
invFun x := ⟨⟨x.1.val * x.2.val, mul_pos x.1.2 x.2.2⟩, ⟨x.1, x.2⟩, by simp [Nat.mem_divisorsAntidiagonal]⟩
left_inv := by
rintro ⟨n, ⟨k, l⟩, h⟩
rw [Nat.mem_divisorsAntidiagonal] at h
ext <;> simp [divisorsAntidiagonalFactors, ← PNat.coe_injective.eq_iff, h.1]
right_inv _ := rfl
