Lean declarations

def strict EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
Strict preference derived from a weak preference relation.
```
def strict {A : Type*} (R : A → A → Prop) (a b : A) : Prop :=
  R a b ∧ ¬ R b a
```
def indiff EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
Indifference derived from a weak preference relation.
```
def indiff {A : Type*} (R : A → A → Prop) (a b : A) : Prop :=
  R a b ∧ R b a
```
def VNM.Completeness EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
**Completeness**: every pair is comparable.
```
def Completeness (pref : A → A → Prop) : Prop :=
  ∀ a b : A, pref a b ∨ pref b a
```
def VNM.Transitivity EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
**Transitivity**: preference chains compose.
```
def Transitivity (pref : A → A → Prop) : Prop :=
  ∀ a b c : A, pref a b → pref b c → pref a c
```

Modules: EconCSLib.Foundation.Preference

Abstract Preference-Relation Axioms

For arguments that quantify over an arbitrary binary relation pref : α → α → Prop (rather than the bundled Preorder instance), the foundation layer exposes a relation-style vocabulary:

Strict preference strict pref a b := pref a b ∧ ¬ pref b a
Indifference indiff pref a b := pref a b ∧ pref b a
Completeness Completeness pref := ∀ a b, pref a b ∨ pref b a
Transitivity Transitivity pref := ∀ a b c, pref a b → pref b c → pref a c

This vocabulary is what preference-based statements and the vNM axiom suite use to formulate axioms about a free-standing relation argument, without committing to the Preorder typeclass on α. Lottery-specific axioms (Independence, Continuity, Archimedean property) are stated on top of Completeness and Transitivity in Utility.VNMAxioms.

In Lean, strict and indiff are library-wide definitions. Completeness and Transitivity remain inside namespace VNM because they name axioms in the vNM suite.

References

[MSZ, Chapter 2] Maschler, Solan, and Zamir, Game Theory. Preference-relation axioms in their relation-style formulation.

Used by

Preference Relation (MSZ Ch.2 Narrative)

Abstract Preference-Relation Axioms

References

Used by

Also in