borelize

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Borelize.borelize

Lean4

/-- Given a type `$t`, if there is an assumption `[i : MeasurableSpace $t]`, then try to prove
`[BorelSpace $t]` and replace `i` with `borel $t`. Otherwise, add instances
`borel $t : MeasurableSpace $t` and `⟨rfl⟩ : BorelSpace $t`. -/
def borelize (t : Term) : TacticM Unit :=
  withMainContext <| do
    let u ← mkFreshLevelMVar
    let e ← withoutRecover <| Tactic.elabTermEnsuringType t (mkSort (mkLevelSucc u))
    let i? ← findLocalDeclWithType? (← mkAppOptM ``MeasurableSpace #[e])
    i?.elim (addBorelInstance e) (borelToRefl e)

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

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

Разделы

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

Аффилиация

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