length_dropSlice_lt

Mathlib.Data.List.TakeDrop

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

English

See previous lemma; length is strictly less under the same hypotheses.

Русский

См. предыдущую лемму; длина строго меньше при тех же гипотезах.

LaTeX

$$$\\text{(see previous lemma)}$$$

Lean4

theorem length_dropSlice_lt (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) :
    (dropSlice i j xs).length < xs.length := by grind

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

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

Разделы

Аффилиация

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