Hartogs.lean

1import Mathlib.SetTheory.Ordinal.Family2import Mathlib.Logic.Small.Basic34/-! # The size obstruction used to terminate sign propagation -/56namespace BFPP78set_option autoImplicit false910universe u1112/-- The ordinals in a universe cannot inject into a type in that same universe. -/13theorem no_injection_from_ordinals (X : Type u) (f : Ordinal.{u} → X) :14    ¬ Function.Injective f := by15  intro hf16  letI : Small.{u} Ordinal.{u} := small_of_injective hf17  have hb : BddAbove (Set.univ : Set Ordinal.{u}) := Ordinal.bddAbove_of_small18  exact not_bddAbove_univ hb1920end BFPP

SHA-256