filter_false

Mathlib.Data.List.Basic

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

English

Filtering a list with the always-false predicate yields the empty list.

Русский

Фильтрация списка по предикату, равному лжи, даёт пустой список.

LaTeX

$$$ \\text{filter}\\ (\\lambda x. \\text{Bool.false})\\ l = [] $$$

Lean4

@[simp]
theorem filter_false (l : List α) : filter (fun _ => false) l = [] := by induction l <;> simp [*, filter]

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

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

Разделы

Аффилиация

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