estimate — Mathlib

English

The current best lower bound for the priority of a node is given by bound (prio n.key) n.estimator.

Русский

Текущее лучшее нижнее ограничение приоритета узла задаётся bound (prio n.key) n.estimator.

LaTeX

$$BestFirstNode.estimate(n) = bound (prio n.key) n.estimator$$

Lean4

/-- Calculate the current best lower bound for the priority of a node. -/
def estimate (n : BestFirstNode prio ε) : ω :=
  bound (prio n.key) n.estimator

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