typein_injective — Mathlib

English

Let (α, r) be a well-ordered set. Then the map a ↦ typein r a is injective; distinct elements have distinct initial-segment types.

Русский

Пусть (α, r) is хорошо упорядочено. Тогда отображение a ↦ typein r a инъективно; различные элементы имеют различные ранги начального отрезка.

LaTeX

$$$\\forall a,b \\in \\alpha,\\ typein_r(a) = typein_r(b) \\Rightarrow a=b$$$

Lean4

theorem typein_injective (r : α → α → Prop) [IsWellOrder α r] : Injective (typein r) :=
  (typein r).injective

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