rec

Mathlib.Data.EReal.Basic

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

Lean4

/-- A recursor for `EReal` in terms of the coercion.

When working in term mode, note that pattern matching can be used directly. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
protected def rec {motive : EReal → Sort*} (bot : motive ⊥) (coe : ∀ a : ℝ, motive a) (top : motive ⊤) :
    ∀ a : EReal, motive a
  | ⊥ => bot
  | (a : ℝ) => coe a
  | ⊤ => top

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

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

Разделы

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

Аффилиация

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