UDom

Definition

DiscreteConvex_EconomicEquilibriumB_UDom

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

discrete-convex-analysis

The effective domain $\operatorname{dom}U=\{x\in\mathbb Z^K:U(x)\ne-\infty\}$ of a utility-type function.

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

Definition code

import Mathlib

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- The effective domain `dom U = {x ∈ Zᴷ : U(x) ≠ −∞}` of a utility-type function. -/
def UDom (U : (K → ℤ) → WithBot ℝ) : Set (K → ℤ) := {x | U x ≠ ⊥}

end DiscreteConvex.EconomicEquilibriumB

Source

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

View graph