getMorphismTheorems

Mathlib.Tactic.FunProp.Theorems

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

Lean4

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

For example calling on `e` equal to `Continuous f` for `f : X→L[ℝ] Y` would return theorem
inferring continuity from the bundled morphism. -/
def getMorphismTheorems (e : Expr) : FunPropM (Array GeneralTheorem) := do
  let thms := (← get).morTheorems.theorems
  let (candidates, thms) ←
    withConfig (fun cfg => { cfg with iota := false, zeta := false }) <| thms.getMatch e false true
  modify ({ · with morTheorems := ⟨thms⟩ })
  return (← MonadExcept.ofExcept candidates).toArray

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

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

Разделы

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

Аффилиация

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