t — Mathlib · SciLib

English

The stable letter t is a distinguished element of the HNN extension, which together with the embedding of G generates the extension.

Русский

Устойчивую букву t можно выбрать как отличительный элемент HNN-расширения; она вместе с вложением G порождает расширение.

LaTeX

$$$ t \\in HNNExtension G A B φ $$$

Lean4

/-- The stable letter of the `HNNExtension` -/
def t : HNNExtension G A B φ :=
  (HNNExtension.con G A B φ).mk'.comp inr (ofAdd 1)

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