length_map — Mathlib

English

For any f: α → β and x ∈ FreeSemigroup α, the length is preserved under map: length(map f x) = length x.

Русский

При отображении по f длина сохраняется: length(map f x) = length x.

LaTeX

$$$\operatorname{length}(\text{map } f \, x) = \operatorname{length}(x)$$$

Lean4

@[to_additive (attr := simp)]
theorem length_map (x) : (map f x).length = x.length :=
  FreeSemigroup.recOnMul x (fun _ ↦ rfl) (fun x y hx hy ↦ by simp only [map_mul, length_mul, *])

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