asString_eq

Mathlib.Data.String.Basic

URI: https://scilib.ai/kg/mathlib#List.asString_eq

English

l.asString = s if and only if l = s.toList.

Русский

l.asString = s тогда и только тогда, когда l = s.toList.

LaTeX

$$$ l.asString = s \iff l = s.toList. $$$

Lean4

theorem asString_eq {l : List Char} {s : String} : l.asString = s ↔ l = s.toList := by
  rw [← asString_toList s, asString_inj, asString_toList s]

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

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

Разделы

Аффилиация

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