chainTopCoeff_reflectionPerm_right

English

Similarly, the top coefficient after reflecting j by itself equals the bottom coefficient with i and j swapped as needed.

Русский

Аналогично, верхний коэффициент после отражения j самим собой равен нижнему коэффициенту при необходимости обмена i и j.

LaTeX

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

Lean4

@[simp]
theorem chainTopCoeff_reflectionPerm_right : P.chainTopCoeff i (P.reflectionPerm j 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_right_aux]
  refine le_antisymm ?_ ?_
  · simpa using this (P.chainTopCoeff i (-j))
  · simpa using this (P.chainBotCoeff i j)

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