rec

Mathlib.Analysis.Normed.Lp.WithLp

URI: https://scilib.ai/kg/mathlib#WithLp.rec

Lean4

/-- A recursor for `WithLp p V`, that reduces to the underlying space `V`.

This unfortunately cannot be registered with `cases_eliminator`, but it can still be used as
`cases v using WithLp.rec with | toLp v =>`. -/
@[elab_as_elim]
protected def rec {motive : WithLp p V → Sort*} (toLp : ∀ v : V, motive (toLp p v)) : ∀ v, motive v := fun v =>
  toLp (ofLp v)

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

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

Разделы

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

Аффилиация

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