idxOf_append_of_mem — Mathlib

English

If a is in l1, then in the concatenation l1 ++ l2, the first occurrence of a is found in l1, i.e., idxOf a (l1 ++ l2) = idxOf a l1.

Русский

Если a принадлежит l1, то в конкатенации l1 ++ l2 первая встреча a находится в l1, то есть idxOf a (l1 ++ l2) = idxOf a l1.

LaTeX

$$$ a \in l_1 \rightarrow \mathrm{idxOf}(a, l_1 \;\|\; l_2) = \mathrm{idxOf}(a, l_1) $$$

Lean4

theorem idxOf_append_of_mem {a : α} (h : a ∈ l₁) : idxOf a (l₁ ++ l₂) = idxOf a l₁ := by grind

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