Lean declarations

def Indifferent EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
```
def Indifferent (a b : A) : Prop := a ≤ b ∧ b ≤ a
```
theorem Indifferent.refl EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
Indifference is reflexive.
```
theorem Indifferent.refl (a : A) : Indifferent a a
```
theorem Indifferent.symm EconCSLib @ cef01c7, EconCSLib.Foundation.Preference
Indifference is symmetric.
```
theorem Indifferent.symm {a b : A} (h : Indifferent a b) : Indifferent b a
```

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

Indifference is transitive.

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

Modules: EconCSLib.Foundation.Preference

Indifference Relation

On any Preorder α, two elements are indifferent when each is weakly preferred to the other: $$ \operatorname{Indifferent}(a, b) \quad\Longleftrightarrow\quad a \le b \;\text{ and }\; b \le a. $$

Indifference is reflexive, symmetric, and transitive. It is therefore an equivalence relation on every preorder. On a PartialOrder antisymmetry collapses it to equality; on a general preorder (or total preorder) it can relate genuinely distinct elements, which is the typical situation in utility theory.

In Lean this is Indifferent : α → α → Prop together with Indifferent.refl / symm / trans.

References

[MSZ, Chapter 2, Def. 2.5] Maschler, Solan, and Zamir, Game Theory. Indifference as the symmetric part of weak preference.

Indifference Relation

References

Used by

Also in