length_le_encode

Mathlib.Logic.Equiv.List

URI: https://scilib.ai/kg/mathlib#Encodable.length_le_encode

← MathLib Explorer

English

For every list l, the length of l is less than or equal to its encoding.

Русский

Для любого списка длина списка не превышает его кодирование.

LaTeX

$$$\\forall l, \\; \\mathrm{length}(l) \\le \\mathrm{encode}(l)$$$

Lean4

theorem length_le_encode : ∀ l : List α, length l ≤ encode l
  | [] => Nat.zero_le _
  | _ :: l => succ_le_succ <| (length_le_encode l).trans (right_le_pair _ _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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