destutter'_ne_nil

Mathlib.Data.List.Destutter

URI: https://scilib.ai/kg/mathlib#List.destutter'_ne_nil

English

For any l and a, l.destutter' R a is not empty.

Русский

Для любых l и a, l.destutter' R a не пуст.

LaTeX

$$$$l.destutter'\,R\,a \neq \varnothing.$$$$

Lean4

theorem destutter'_ne_nil : l.destutter' R a ≠ [] :=
  ne_nil_of_mem <| l.mem_destutter' R a

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

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

Разделы

Аффилиация

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