Lean declarations

structure RepresentsPreference EconCSLib @ cef01c7, EconCSLib.Foundation.Preference

structure RepresentsPreference [Preorder A] [Preorder V] (u : A → V) : Prop where
  /-- The representation property: `a ≤ b ↔ u(a) ≤ u(b)`. -/
  le_iff : ∀ a b : A, a ≤ b ↔ u a ≤ u b

theorem RepresentsPreference.lt_iff EconCSLib @ cef01c7, EconCSLib.Foundation.Preference

A utility representation preserves strict preference.

theorem RepresentsPreference.lt_iff [Preorder A] [Preorder V] {u : A → V}
    (h : RepresentsPreference u) (a b : A) :
    a < b ↔ u a < u b

theorem RepresentsPreference.indifferent_iff EconCSLib @ cef01c7, EconCSLib.Foundation.Preference

A utility representation preserves indifference.

theorem RepresentsPreference.indifferent_iff [Preorder A] [Preorder V] {u : A → V}
    (h : RepresentsPreference u) (a b : A) :
    Indifferent a b ↔ Indifferent (u a) (u b)

Modules: EconCSLib.Foundation.Preference

Utility Representation of a Preference

Given preorders on α and β, a function u : α → β represents the preference ≤ on α when it preserves and reflects weak preference: $$ \forall a,\,b,\quad a \le b \;\Longleftrightarrow\; u(a) \le u(b). $$

A representation automatically preserves the derived strict preference and indifference relations, witnessed by RepresentsPreference.lt_iff and RepresentsPreference.indifferent_iff. This is the abstract scaffolding used by ordinal-utility statements in utility theory (the foundation.preference topic) and by vNM-style expected-utility theorems.

In Lean this is structure RepresentsPreference (u : α → β) : Prop carrying the single field le_iff. The two derived iff lemmas are stated and proved directly from le_iff using the Mathlib Preorder API.

References

[MSZ, Chapter 2, Def. 2.7] Maschler, Solan, and Zamir, Game Theory. Utility representation of a preference relation.

Used by

Expected Utility Representation

Utility Representation of a Preference

References

Used by

Also in