not_surjective_of_ordinal — Mathlib

English

For every α with Small α and every function f: α → Ordinal, f is not surjective.

Русский

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

LaTeX

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

Lean4

theorem not_surjective_of_ordinal {α : Type*} [Small.{u} α] (f : α → Ordinal.{u}) : ¬Surjective f :=
  by
  intro h
  obtain ⟨a, ha⟩ := h (⨆ i, succ (f i))
  apply ha.not_lt
  rw [Ordinal.lt_iSup_iff]
  exact ⟨a, Order.lt_succ _⟩

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