instOrdBestFirstNode

Mathlib.Deprecated.MLList.BestFirst

URI: https://scilib.ai/kg/mathlib#instOrdBestFirstNode

English

Once an fstInst estimator is constructed, it respects the ordering of bounds of the first component.

Русский

Построенный fstInst-оцениватель сохраняет порядок по пределам первого компонента.

LaTeX

$$fstInst congr_simp$$

Lean4

instance [Ord ω] [Ord α] : Ord (BestFirstNode prio ε) where
  compare := compareLex (compareOn BestFirstNode.estimate) (compareOn BestFirstNode.key)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru