P3_of_ih — Mathlib

English

Under hy and IH1 y x, P3 holds for left moves i, k and left y-move l with the negation of y moved left.

Русский

При hy и IH1 y x выполняется P3 при i, k и l, учитывая движение слева от -y.

LaTeX

$$$P3\\ (x.moveLeft i)\\ x\\ (y.moveLeft k)\\ (-(-y).moveLeft l)$$$

Lean4

theorem P3_of_ih (hy : Numeric y) (ihyx : IH1 y x) (i k l) : P3 (x.moveLeft i) x (y.moveLeft k) (-(-y).moveLeft l) :=
  P3_comm.2 <|
    ((ihyx (IsOption.moveLeft k) (isOption_neg.1 <| .moveLeft l) <| Or.inl rfl).2
          (by rw [moveLeft_neg, neg_neg]; apply hy.left_lt_right)).1
      i

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