longestPrefix — Mathlib

English

The longestPrefix x s equals shortestPrefixDiff x s minus 1.

Русский

longestPrefix(x,s) = shortestPrefixDiff(x,s) − 1.

LaTeX

$$$$ \text{longestPrefix}(x,s) = \text{shortestPrefixDiff}(x,s) - 1 $$$$

Lean4

/-- Given a point `x` in a product space `Π (n : ℕ), E n`, and `s` a subset of this space, then
`longestPrefix x s` if the largest `n` for which there is an element of `s` having the same
prefix of length `n` as `x`. If there is no such `n`, use `0` by convention. -/
def longestPrefix {E : ℕ → Type*} (x : ∀ n, E n) (s : Set (∀ n, E n)) : ℕ :=
  shortestPrefixDiff x s - 1

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