Non-Injectivity of Ordinal-limited Function

Stream: general

[Ira Fesefeldt]

I am trying to prove that a function defined on ordinals f : Ordinal → α is not injective in the first Order.Succ #α elements. However, I am a bit stuck there. I have something like:

variable (g: Ordinal → α)

def limitation : { i : Ordinal // i < (Cardinal.ord $ Order.succ #α)} → α := λ i => g i

lemma limitation_eq : ∀ i, limitation g i = g i := by
  intro h; unfold limitation; exact rfl

lemma cardinal_no_max : ∀ ℵ : Cardinal, ¬ IsMax ℵ := by
  intro ℵ h
  unfold IsMax at h; specialize h (le_of_lt $ Cardinal.cantor ℵ)
  exact not_lt_of_le h (Cardinal.cantor ℵ)

lemma limitation_not_injective: ¬ Injective (limitation g) := by
  intro h_inj
  have h₁ : Order.succ #α ≤ #α := by apply Cardinal.mk_le_of_injective h_inj; sorry
  have h₂ : #α < Order.succ #α := Order.lt_succ_of_not_isMax (cardinal_no_max #α)
  exact not_le_of_lt h₂ h₁

However, Cardinal.mk_le_of_injective does not work since the domain and codomain live in different universes. Anyone maybe a pointer how to handle this?

[Yaël Dillies]

Use docs#Cardinal.lift_mk_le_lift_mk_of_injective instead