length_eq_list_length

Mathlib.Data.String.Lemmas

URI: https://scilib.ai/kg/mathlib#String.length_eq_list_length

English

For any list l, the length of the string mk l equals l.length.

Русский

Для любого списка l длина строки mk l равна длине списка l.

LaTeX

$$$ \forall l:\text{List Char},\ (\text{String.mk } l).length = l.length. $$$

Lean4

theorem length_eq_list_length (l : List Char) : (String.mk l).length = l.length := by simp only [String.length]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru