sym2_eq_nil_iff

Mathlib.Data.List.Sym

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

English

xs.sym2 is empty exactly when xs is empty.

Русский

xs.sym2 пуст, если xs пуст.

LaTeX

$$$$ xs.sym2 = \\emptyset \\quad\\Longleftrightarrow\\quad xs = [] $$$$

Lean4

@[simp]
theorem sym2_eq_nil_iff {xs : List α} : xs.sym2 = [] ↔ xs = [] := by cases xs <;> simp [List.sym2]

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

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

Разделы

Аффилиация

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