reduceOption_length_le

Mathlib.Data.List.ReduceOption

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

← MathLib Explorer

English

The length of the reduced option list is at most the length of the original list.

Русский

Длина reduceOption(l) не превышает длину l.

LaTeX

$$$|\mathrm{reduceOption}(l)| \leq |l|$$$

Lean4

theorem reduceOption_length_le (l : List (Option α)) : l.reduceOption.length ≤ l.length :=
  by
  rw [length_eq_reduceOption_length_add_filter_none]
  apply Nat.le_add_right

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

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

Разделы

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

Аффилиация

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