cons_injective

Mathlib.Data.List.Basic

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

English

The function a ↦ [a] (mapping an element to its singleton list) is injective; i.e., if [a] = [b] then a = b.

Русский

Функция a ↦ [a] инъективна; если [a] = [b], то a = b.

LaTeX

$$∀ a b, [a] = [b] → a = b$$

Lean4

@[simp]
theorem cons_injective {a : α} : Injective (cons a) := fun _ _ => tail_eq_of_cons_eq

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

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

Разделы

Аффилиация

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