cons_not_rev

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.Red.Step.cons_not_rev

English

Prepending (x, ¬b) and then (x, b) reduces in one step: Red.Step ((x, ¬b) :: (x, b) :: L) L.

Русский

Предпосылание (x,¬b) затем (x,b) редуцируется за один шаг: Red.Step ((x,¬b) :: (x,b) :: L) L.

LaTeX

$$$ \\mathrm{Red}.\\mathrm{Step}\\bigl((x, \\lnot b) :: (x, b) :: L\\bigr)\\; L$$$

Lean4

@[to_additive (attr := simp)]
theorem cons_not_rev {x b} : Red.Step ((x, !b) :: (x, b) :: L) L :=
  @Red.Step.not_rev _ [] _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru