buildTransitiveLeProof

Mathlib.Tactic.Order.Graph.Basic

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Order.Graph.buildTransitiveLeProof

Lean4

/-- Given a `≤`-graph `g`, finds a proof of `s ≤ t` using transitivity. -/
def buildTransitiveLeProof (g : Graph) (idxToAtom : Std.HashMap Nat Expr) (s t : Nat) : MetaM (Option Expr) := do
  let state : DFSState := ⟨.replicate g.size false⟩
  (buildTransitiveLeProofDFS g s t (idxToAtom.get! t)).run' state

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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