append_right_injective

Mathlib.Data.Stream.Init

URI: https://scilib.ai/kg/mathlib#Stream'.append_right_injective

Lean4

theorem append_right_injective (h : x ++ₛ a = x ++ₛ b) : a = b := by ext n;
  replace h := congr_arg (fun a ↦ a.get (x.length + n)) h; simpa using h

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

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

Разделы

Аффилиация

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