length — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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