not_injective_of_ordinal — Mathlib

English

For every Small α, any function f: Ordinal → α cannot be injective.

Русский

Для каждого малого типа α любая функция f: Ordinal → α не инъективна.

LaTeX

$$$\\forall \\alpha\\ [Small(\\alpha)]\\ (f: Ordinal \\to \\alpha)\\; \\neg Injective(f)$$$

Lean4

theorem not_injective_of_ordinal {α : Type*} [Small.{u} α] (f : Ordinal.{u} → α) : ¬Injective f := fun h ↦
  not_surjective_of_ordinal _ (invFun_surjective h)

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