signBijAux_injOn — Mathlib

English

The map signBijAux is injective on the domain of finite pairs, when restricted to finPairsLT.

Русский

Отображение signBijAux инъективно на области финальных пар, ограниченной finPairsLT.

LaTeX

$$$ (finPairsLT n : Set (\\Sigma _ : Fin n, Fin n)).InjOn (signBijAux f) $$$

Lean4

theorem signBijAux_injOn {n : ℕ} {f : Perm (Fin n)} : (finPairsLT n : Set (Σ _, Fin n)).InjOn (signBijAux f) :=
  by
  rintro ⟨a₁, a₂⟩ ha ⟨b₁, b₂⟩ hb h
  dsimp [signBijAux] at h
  rw [Finset.mem_coe, mem_finPairsLT] at *
  have : ¬b₁ < b₂ := hb.le.not_gt
  split_ifs at h <;> simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]
  · exact absurd this (not_le.mpr ha)
  · exact absurd this (not_le.mpr ha)

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