English
Under suitable noninjectivity conditions and a top element, there exists j with transfiniteIterate φ j i₀ = ⊤.
Русский
При удовлетворяющих условиях неинъективности и наличии верхнего элемента существует j такое, что transfiniteIterate φ j i₀ = ⊤.
LaTeX
$$$\\exists j:\\\\ J,\\\\ transfiniteIterate φ j i_0 = \\top$$$
Lean4
theorem top_mem_range_transfiniteIterate (hφ' : ∀ i ≠ (⊤ : I), i < φ i) (φtop : φ ⊤ = ⊤)
(H : ¬Function.Injective (fun (j : J) ↦ transfiniteIterate φ j i₀)) : ∃ (j : J), transfiniteIterate φ j i₀ = ⊤ :=
by
have hφ (i : I) : i ≤ φ i := by
by_cases hi : i = ⊤
· subst hi
rw [φtop]
· exact (hφ' i hi).le
obtain ⟨j₁, j₂, hj, eq⟩ : ∃ (j₁ j₂ : J) (hj : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀ :=
by
dsimp [Function.Injective] at H
simp only [not_forall] at H
obtain ⟨j₁, j₂, eq, hj⟩ := H
by_cases hj' : j₁ < j₂
· exact ⟨j₁, j₂, hj', eq⟩
· simp only [not_lt] at hj'
obtain hj' | rfl := hj'.lt_or_eq
· exact ⟨j₂, j₁, hj', eq.symm⟩
· simp at hj
by_contra!
suffices transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀ by simp only [eq, lt_self_iff_false] at this
have hj₁ : ¬IsMax j₁ := by
simp only [not_isMax_iff]
exact ⟨_, hj⟩
refine lt_of_lt_of_le (hφ' _ (this j₁)) ?_
rw [← transfiniteIterate_succ φ i₀ j₁ hj₁]
exact monotone_transfiniteIterate _ _ hφ (Order.succ_le_of_lt hj)
