length_map — Mathlib

English

If (s.map f) terminates with h, then its length equals the length of s under the corresponding termination proof.

Русский

Если (s.map f) завершается с доказательством h, то его длина равна длине s под соответствующим доказательством завершения.

LaTeX

$$$\forall {s : Seq \alpha} {f : \alpha \to \beta} (h : (s.map f).Terminates),\; (s.map f).length h = s.length (terminates_map_iff.1 h)$$$

Lean4

@[simp]
theorem length_map {s : Seq α} {f : α → β} (h : (s.map f).Terminates) :
    (s.map f).length h = s.length (terminates_map_iff.1 h) :=
  by
  rw [length]
  congr
  ext
  simp

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