Theorems · Definition · order theory

EReal.rec

{motive : EReal → Sort u_1} → motive ⊥ → ((a : ℝ) → motive ↑a) → motive ⊤ → (a : EReal) → motive a

A recursor for EReal in terms of the coercion. When working in term mode, note that pattern matching can be used directly, although this is prone to leaking the implementation details in terms of Option.

Defined in

Mathlib.Data.EReal.Basic

Cited by

57 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms