length — Mathlib

English

The length function on FreeMagma is defined by length(of x) = 1 and length(u * v) = length(u) + length(v).

Русский

Функция длины на FreeMagma задаётся так: длина(of x) = 1 и длина( u * v ) = длина(u) + длина(v).

LaTeX

$$$\operatorname{length} : \mathrm{FreeMagma} \alpha \to \mathbb{N},\quad \operatorname{length}(\mathrm{of}(x)) = 1,\quad \operatorname{length}(u \ast v) = \operatorname{length}(u) + \operatorname{length}(v)$$$

Lean4

/-- Length of an element of a free magma. -/
def length {α : Type u} : FreeMagma α → ℕ
  | FreeMagma.of _x => 1
  | x * y => x.length + y.length

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