chainBotCoeff_reflectionPerm_right

English

Under reflection, the bottom coefficient with i and j equals the top coefficient with i and j swapped accordingly.

Русский

При отражении снизу коэффициент с i и j соответствует верхнему коэффициенту с i и j переставленными.

LaTeX

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

Lean4

@[simp]
theorem chainBotCoeff_reflectionPerm_right : P.chainBotCoeff i (P.reflectionPerm j j) = P.chainTopCoeff 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.chainBotCoeff i (-j))
  · simpa using this (-P.chainTopCoeff i j)

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