idxOf_of_notMem

Mathlib.Data.List.Basic

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

English

If a is not in l, then idxOf a l equals the length of l.

Русский

Если a не принадлежит l, то idxOf a l равно длине l.

LaTeX

$$$ a \notin l \rightarrow \mathrm{idxOf}(a, l) = |l| $$$

Lean4

@[simp]
theorem idxOf_of_notMem {l : List α} {a : α} : a ∉ l → idxOf a l = length l :=
  idxOf_eq_length_iff.2

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

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

Разделы

Аффилиация

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