signBijAux_mem — Mathlib

English

For every n and f ∈ Perm(Fin(n)), if a ∈ finPairsLT n then signBijAux f a ∈ finPairsLT n.

Русский

Пусть n и f ∈ Perm(Fin(n)). Если a ∈ finPairsLT n, то signBijAux(f, a) ∈ finPairsLT n.

LaTeX

$$$\forall n, \forall f \in \mathrm{Perm}(\mathrm{Fin}(n)),\ a \in \mathrm{finPairsLT}(n) \to signBijAux(f,a) \in \mathrm{finPairsLT}(n)$$$

Lean4

theorem signBijAux_mem {n : ℕ} {f : Perm (Fin n)} :
    ∀ a : Σ _ : Fin n, Fin n, a ∈ finPairsLT n → signBijAux f a ∈ finPairsLT n := fun ⟨a₁, a₂⟩ ha =>
  by
  unfold signBijAux
  split_ifs with h
  · exact mem_finPairsLT.2 h
  · exact mem_finPairsLT.2 ((le_of_not_gt h).lt_of_ne fun h => (mem_finPairsLT.1 ha).ne (f.injective h.symm))

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