toList_inj

Mathlib.Data.String.Basic

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

English

The map s ↦ s.toList is injective: if s1.toList = s2.toList then s1 = s2.

Русский

Отображение строк в списки символов инъективно: если s1.toList = s2.toList, то s1 = s2.

LaTeX

$$$ s_1.toList = s_2.toList \iff s_1 = s_2. $$$

Lean4

theorem toList_inj {s₁ s₂ : String} : s₁.toList = s₂.toList ↔ s₁ = s₂ :=
  ⟨congr_arg mk, congr_arg toList⟩

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

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

Разделы

Аффилиация

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