val_unique

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.Results.val_unique

English

If s has two results a with m and b with n, then a = b.

Русский

Если у s есть два результата a и b с длиннами m и n, то a = b.

LaTeX

$$$\forall s\ {a}\ {b}\ {m}\ {n},\; \text{Results } s a m \rightarrow \text{Results } s b n \rightarrow a = b$$$

Lean4

theorem val_unique {s : Computation α} {a b m n} (h1 : Results s a m) (h2 : Results s b n) : a = b :=
  mem_unique h1.mem h2.mem

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

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

Разделы

Аффилиация

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