length'_map — Mathlib

English

The extended length length' is preserved by map: (s.map f).length' = s.length'.

Русский

Расширенная длина length' сохраняется под отображением: (s.map f).length' = s.length'.

LaTeX

$$$(s.map f).length' = s.length'$$$

Lean4

@[simp]
theorem length'_map {s : Seq α} {f : α → β} : (s.map f).length' = s.length' :=
  by
  by_cases h : (s.map f).Terminates <;> have h' := h <;> rw [terminates_map_iff] at h'
  · rw [length'_of_terminates h, length'_of_terminates h', length_map h]
  · rw [length'_of_not_terminates h, length'_of_not_terminates h']

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