chainTopCoeff_reflectionPerm_left

English

When applying the reflection permutation to i with itself, the top coefficient against j equals the bottom coefficient against j.

Русский

При применении отражательной перестановки к i относительно самого i, верхний коэффициент по отношению к j равен нижнему коэффициенту по отношению к j.

LaTeX

$$$$ P.chainTopCoeff(P.reflectionPerm(i,i), j) = P.chainBotCoeff(i, j) $$$$

Lean4

@[simp]
theorem chainTopCoeff_reflectionPerm_left : P.chainTopCoeff (P.reflectionPerm i i) j = P.chainBotCoeff i j :=
  by
  letI := P.indexNeg
  have (z : ℤ) :
    z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
      z ∈ Icc (-P.chainBotCoeff (-i) j : ℤ) (P.chainTopCoeff (-i) j) :=
    by rw [P.chainCoeff_reflectionPerm_left_aux]
  refine le_antisymm ?_ ?_
  · simpa using this (P.chainTopCoeff (-i) j)
  · simpa using this (P.chainBotCoeff i j)

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