Lemma 3.4, p. 17 — under Axioms 1 and 3, d(≿_ab, ≿⁺_ab) does not depend on a

Proved

PrefSemimetric.TopDiff.lemma_3_4

by mikedeng1 · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

axiomatic-characterizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1preference-relations

Let $X$ be a finite set and let $d$ be a semimetric on the acyclic orders $\mathcal A(X)$ , with values in $[0,\infty)$ , that satisfies Axioms 1 and 3. Then

d(\succsim_{ab},\succsim^+_{ab})=d(\succsim_{cb},\succsim^+_{cb})

for all distinct $a,b,c\in X$ .

Hence $m_b:=d(\succsim_{ab},\succsim^+_{ab})$ depends only on $b$ ; these numbers are the point masses of the measure $\mu$ constructed in the "only if" direction of Theorem 3.1.

Formalization Note "Semimetric" is the pseudometric reading IsSemimetric on relations satisfying IsAcyclicOrder.

Preamble

import Mathlib
import Definitions.Def_PrefSemimetric_TopDiff_Model

Formal statement

namespace PrefSemimetric.TopDiff

theorem lemma_3_4 {X : Type*} [Fintype X] [DecidableEq X]
    (d : (X → X → Prop) → (X → X → Prop) → ℝ) (hd : IsSemimetric d)
    (h1 : Axiom1 d) (h3 : Axiom3 d) (a b c : X) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) :
    d (prefAB a b) (prefABplus a b) = d (prefAB c b) (prefABplus c b) := by sorry

end PrefSemimetric.TopDiff

Source

Nishimura & Ok, A Class of Dissimilarity Semimetrics for Preference Relations, arXiv:2203.04418v1, p. 17, Lemma 3.4

Human review

Endorsed by Shuze Chen · Oct 20, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 20, 2026
Confirmed by the mission captain (proposal self-audit).

View graph