height_sub — Mathlib

English

If the root k equals the difference P.root i minus P.root j, then height(k) equals height(i) minus height(j).

Русский

Если корень k равен разности P.root i и P.root j, то высота k равна разности высот i и j.

LaTeX

$$$P.root\ k = P.root\ i - P.root\ j \Rightarrow b.height\ k = b.height\ i - b.height\ j$$$

Lean4

theorem height_sub {i j k : ι} (hk : P.root k = P.root i - P.root j) : b.height k = b.height i - b.height j :=
  by
  letI := P.indexNeg
  replace hk : P.root k = P.root i + P.root (-j) := by simpa [← sub_eq_add_neg]
  rw [sub_eq_add_neg, ← b.height_reflectionPerm_self, b.height_add hk]

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