getTransitionTheorems

Mathlib.Tactic.FunProp.Theorems

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.getTransitionTheorems

Lean4

/-- Get transition theorems applicable to `e`.

For example calling on `e` equal to `Continuous f` might return theorems implying continuity
from linearity over finite-dimensional spaces or differentiability. -/
def getTransitionTheorems (e : Expr) : FunPropM (Array GeneralTheorem) := do
  let thms := (← get).transitionTheorems.theorems
  let (candidates, thms) ←
    withConfig (fun cfg => { cfg with iota := false, zeta := false }) <| thms.getMatch e false true
  modify ({ · with transitionTheorems := ⟨thms⟩ })
  return (← MonadExcept.ofExcept candidates).toArray

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

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

Разделы

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

Аффилиация

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