English
There exists a function g from ordinals to an arbitrary set such that g is not injective on a certain initial segment of ordinals indexed below the successor of the cardinality of the domain.
Русский
Существует функция g: Ordinal → α, которая не инъективна на заданном начальном отрезке ординалов, ограниченном справа переходом к succ Cardinal.mk α.
LaTeX
$$$ \\neg \\operatorname{InjOn} \\, g \\bigl(Iio(\\operatorname{ord}(<|>\\operatorname{succ}|#\\alpha))\\bigr) $$$
Lean4
theorem not_injective_limitation_set : ¬InjOn g (Iio (ord <| succ #α)) :=
by
intro h_inj
have h := lift_mk_le_lift_mk_of_injective <| injOn_iff_injective.1 h_inj
have mk_initialSeg_subtype : #(Iio (ord <| succ #α)) = lift.{u + 1} (succ #α) := by
simpa only [coe_setOf, card_typein, card_ord] using mk_Iio_ordinal (ord <| succ #α)
rw [mk_initialSeg_subtype, lift_lift, lift_le] at h
exact not_le_of_gt (Order.lt_succ #α) h
