ToERealOfBot

Definition

DiscreteConvex_EconomicEquilibriumB_ToERealOfBot

by Shuze Chen · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-convex-analysis

The canonical embedding $\mathbb R\cup\{-\infty\}\hookrightarrow\mathbb R\cup\{\pm\infty\}$ .

(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.212, redeclared, dualized.)

Definition code

import Mathlib

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- The canonical embedding `R∪{−∞} ↪ R∪{±∞}`. -/
noncomputable def ToERealOfBot (v : WithBot ℝ) : EReal := v.elim ⊥ (fun r => (r : EReal))

end DiscreteConvex.EconomicEquilibriumB

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.212, redeclared, dualized

View graph