ne_nil_of_mem_splitBy

Mathlib.Data.List.SplitBy

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

Lean4

theorem ne_nil_of_mem_splitBy (r : α → α → Bool) {l : List α} (h : m ∈ l.splitBy r) : m ≠ [] :=
  by
  rintro rfl
  exact nil_notMem_splitBy r l h

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

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

Разделы

Аффилиация

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