English
Let n be a natural number and f a permutation of Fin(n). The map a ↦ signBijAux(f, a) from finPairsLT n to itself is surjective; equivalently, for every a ∈ finPairsLT n there exists b ∈ finPairsLT n with signBijAux(f, b) = a.
Русский
Пусть n — натуральное число и f — перестановка Fin(n). Отображение a ↦ signBijAux(f, a) из finPairsLT n в себя сюръективно; эквивалентно: для каждого a ∈ finPairsLT n существует b ∈ finPairsLT n такое, что signBijAux(f, b) = a.
LaTeX
$$$\forall a \in finPairsLT(n), \exists b \in finPairsLT(n),\signBijAux(f,b) = a$$$
Lean4
theorem signBijAux_surj {n : ℕ} {f : Perm (Fin n)} : ∀ a ∈ finPairsLT n, ∃ b ∈ finPairsLT n, signBijAux f b = a :=
fun ⟨a₁, a₂⟩ ha =>
if hxa : f⁻¹ a₂ < f⁻¹ a₁ then
⟨⟨f⁻¹ a₁, f⁻¹ a₂⟩, mem_finPairsLT.2 hxa, by
dsimp [signBijAux]
rw [apply_inv_self, apply_inv_self, if_pos (mem_finPairsLT.1 ha)]⟩
else
⟨⟨f⁻¹ a₂, f⁻¹ a₁⟩,
mem_finPairsLT.2 <| (le_of_not_gt hxa).lt_of_ne fun h => by simp [mem_finPairsLT, f⁻¹.injective h] at ha,
by
dsimp [signBijAux]
rw [apply_inv_self, apply_inv_self, if_neg (mem_finPairsLT.1 ha).le.not_gt]⟩
