Red — Mathlib

English

FreeGroup.Red is defined as the reflexive-transitive closure of Red.Step; it encodes multi-step reductions.

Русский

FreeGroup.Red определяется как рефлексивно-транзитивное замыкание отношения Red.Step и кодирует многошаговые редукции.

LaTeX

$$$ \\text{Red} \\;=\\; \\mathrm{ReflTransGen}(\\text{Red.Step}) $$$

Lean4

/-- Reflexive-transitive closure of `Red.Step` -/
@[to_additive /-- Reflexive-transitive closure of `Red.Step` -/
    ]
def Red : List (α × Bool) → List (α × Bool) → Prop :=
  ReflTransGen Red.Step

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