instSubsingletonOfIsWellOrder — Mathlib

English

For any principal-segment embedding f, f is surjective onto the set of β for which s holds with f.top.

Русский

Для любого встраивания f множество образа f является все β, удовлетворяющее s(b, f.top).

LaTeX

$$$\\text{SurjOn}(f, \\mathrm{Set.univ}, \\{b \\mid s(b, f.top)\\})$$$

Lean4

/-- Given a well order `s`, there is a most one principal segment embedding of `r` into `s`. -/
instance [IsWellOrder β s] : Subsingleton (r ≺i s) where allEq f g := ext ((f : r ≼i s).eq g)

Похожие утверждения