Lean declarations

abbrev StrictlyPreferred EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
Strict preference is just `<` from the preorder. [MSZ 2.5]
```
abbrev StrictlyPreferred (a b : A) : Prop := a < b
```
theorem StrictlyPreferred.asymm EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
Strict preference is asymmetric: `a ≻ b → ¬(b ≻ a)`. [MSZ Ex 2.1(a)]
```
theorem StrictlyPreferred.asymm {a b : A} (h : StrictlyPreferred a b) :
    ¬ StrictlyPreferred b a
```

theorem StrictlyPreferred.trans EconCSLib @ cef01c7, EconCSLib.Foundation.Preference

Strict preference is transitive. [MSZ Ex 2.1(a)]

theorem StrictlyPreferred.trans {a b c : A}
    (h₁ : StrictlyPreferred a b) (h₂ : StrictlyPreferred b c) :
    StrictlyPreferred a c

theorem StrictlyPreferred.irrefl EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
Strict preference is irreflexive. [MSZ Ex 2.1(a)]
```
theorem StrictlyPreferred.irrefl (a : A) : ¬ StrictlyPreferred a a
```

Modules: EconCSLib.Foundation.Preference

Strict Preference Relation

On any Preorder α, strict preference is the strict part of the preorder: $$ a \succ b \quad\Longleftrightarrow\quad a < b \quad\Longleftrightarrow\quad a \le b \;\text{ and }\; \neg(b \le a). $$

Strict preference is asymmetric, transitive, and irreflexive. These three properties — asymmetry from lt_asymm, transitivity from lt_trans, irreflexivity from lt_irrefl — are inherited directly from the Mathlib Preorder API.

In Lean this is abbrev StrictlyPreferred (a b : α) : Prop := a < b. The abbreviation exists for readability in game-theory contexts; downstream code may also use the bare < notation interchangeably.

References

[MSZ, Chapter 2, Def. 2.5] Maschler, Solan, and Zamir, Game Theory. Strict preference derived from weak preference.
[MSZ, Exercise 2.1(a)] Asymmetry, transitivity, and irreflexivity of strict preference.

Strict Preference Relation

References

Used by

Also in