English
If β with s is a well-ordered set under IsTrichotomous and IsIrrefl, and α with r is well-founded, then there is at most one initial segment embedding r ≼i s.
Русский
Если β с s является хорошо упорядоченным при IsTrichotomous и IsIrrefl, и α с r хорошо основан, то отображение InitialSeg r ≼i s единственно.
LaTeX
$$$[IsTrichotomous \\ β\\ s] \\rightarrow [IsIrrefl \\ β\\ s] \\rightarrow [IsWellFounded \\ α \\ r] \\Rightarrow Subsingleton (r ≼i s).$$$
Lean4
instance subsingleton_of_trichotomous_of_irrefl [IsTrichotomous β s] [IsIrrefl β s] [IsWellFounded α r] :
Subsingleton (r ≼i s) where
allEq f
g := by
ext a
refine IsWellFounded.induction r a fun b IH => extensional_of_trichotomous_of_irrefl s fun x => ?_
rw [f.exists_eq_iff_rel, g.exists_eq_iff_rel]
exact exists_congr fun x => and_congr_left fun hx => IH _ hx ▸ Iff.rfl
