find — Mathlib

English

Retrieve an element of an ordered set equivalent to x, if it exists, in logarithmic time.

Русский

Поиск элемента в упорядоченном множестве, эквивалентного x, если такой существует, за временем O(log n).

LaTeX

$$$\\forall x:\\alpha,\\ s:\\mathrm{Ordset}\\alpha,\\; \\mathrm{find}(x,s) = \\mathrm{Ordnode.find}(x,s.\\mathrm{val})$$$

Lean4

/-- O(log n). Retrieve an element in the set that is equivalent to `x` in the order,
  if it exists. -/
def find (x : α) (s : Ordset α) : Option α :=
  Ordnode.find x s.val

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