chainBotCoeff_reflectionPerm_left

English

Under the same reflection, the bottom coefficient equals the top coefficient with i and j interchanged appropriately.

Русский

При том же отражении нижний коэффициент равен верхнему коэффициенту с соответствующим обменом i и j.

LaTeX

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

Lean4

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

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