cons — Mathlib

English

If H is a red step between L1 and L2, then adding the same element x to the front preserves the step: cons {x} H : Red.Step (x :: L1) (x :: L2).

Русский

Если H является переходом между L1 и L2, то добавление одинакового элемента x спереди сохраняет переход: Red.Step (x :: L1) (x :: L2).

LaTeX

$$$ \\forall x\\; (H : \\mathrm{Red.Step}\\; L_1\\; L_2),\\; \\mathrm{Red.Step}(x :: L_1)(x :: L_2).$$$

Lean4

@[to_additive]
theorem cons {x} (H : Red.Step L₁ L₂) : Red.Step (x :: L₁) (x :: L₂) :=
  @Step.append_left _ [x] _ _ H

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