branching

Mathlib.Tactic.Linarith.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.GlobalPreprocessor.branching

Lean4

/-- A `GlobalPreprocessor` lifts to a `GlobalBranchingPreprocessor` by producing only one branch.
-/
def branching (pp : GlobalPreprocessor) : GlobalBranchingPreprocessor
    where
  __ := pp
  transform := fun g l => do
    return [⟨g, ← pp.transform l⟩]

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

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

Разделы

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

Аффилиация

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