idxOf_eq_length_iff

Mathlib.Data.List.Basic

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

English

For any a and list l, idxOf a l equals length l if and only if a is not in l.

Русский

Для любого a и списка l, idxOf a l равно длине l тогда и только тогда, когда a не принадлежит l.

LaTeX

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

Lean4

theorem idxOf_eq_length_iff {a : α} {l : List α} : idxOf a l = length l ↔ a ∉ l := by grind

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

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

Разделы

Аффилиация

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