English
There is a function shortestPrefixDiff x s giving the first index where x and s disagree in a precise sense.
Русский
Функция shortestPrefixDiff(x,s) задаёт первый индекс, на котором x и элементы множества s расходятся в точном смысле.
LaTeX
$$$$ \text{shortestPrefixDiff}(x,s) = \text{the least } n \text{ with a disjoint cylinder from } s $$$$
Lean4
/-- Given a point `x` in a product space `Π (n : ℕ), E n`, and `s` a subset of this space, then
`shortestPrefixDiff x s` if the smallest `n` for which there is no element of `s` having the same
prefix of length `n` as `x`. If there is no such `n`, then use `0` by convention. -/
def shortestPrefixDiff {E : ℕ → Type*} (x : ∀ n, E n) (s : Set (∀ n, E n)) : ℕ :=
if h : ∃ n, Disjoint s (cylinder x n) then Nat.find h else 0
