lookmap_of_forall_not

Mathlib.Data.List.Lookmap

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

English

If every element of l is sent by f to none, then l.lookmap f = l.

Русский

Если каждый элемент списка l отображается в none функцией f, то l.lookmap f = l.

LaTeX

$$$\\forall a\\in l,\\ f\\ a = \\text{none} \\Rightarrow \\mathrm{lookmap}\\ f\\ l = l.$$$

Lean4

theorem lookmap_of_forall_not {l : List α} (H : ∀ a ∈ l, f a = none) : l.lookmap f = l :=
  (lookmap_congr H).trans (lookmap_none l)

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

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

Разделы

Аффилиация

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