ofList_injective — Mathlib

English

The map from lists to sequences is injective: if ofList(l1) = ofList(l2) then l1 = l2.

Русский

Отображение списков в последовательности инъективно: если ofList(l1) = ofList(l2), то l1 = l2.

LaTeX

$$$ \forall l_1,l_2:\mathrm{List}(\alpha),\ ofList(l_1) = ofList(l_2) \Rightarrow l_1 = l_2.$$$

Lean4

theorem ofList_injective : Function.Injective (ofList : List α → _) := fun _ _ h =>
  List.ext_getElem? fun _ => congr_fun (Subtype.ext_iff.1 h) _

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