mem_range_rank_of_le — Mathlib

English

For any o ≤ rank_r(a), there exists b with Acc r b and rank_r(b) = o.

Русский

Пусть o ≤ rank_r(a). Существуют b с Acc r b и rank_r(b) = o.

LaTeX

$$$o \le \operatorname{rank}_r(a) \Rightarrow \exists b \,(\operatorname{Acc}_r(b) \land \operatorname{rank}_r(b) = o)$$$

Lean4

theorem mem_range_rank_of_le {o : Ordinal} (ha : Acc r a) (ho : o ≤ ha.rank) : ∃ (b : α) (hb : Acc r b), hb.rank = o :=
  by
  obtain rfl | ho := ho.eq_or_lt
  · exact ⟨a, ha, rfl⟩
  · revert ho
    refine ha.recOn fun a ha IH ho ↦ ?_
    rw [rank_eq, Ordinal.lt_iSup_iff] at ho
    obtain ⟨⟨b, hb⟩, ho⟩ := ho
    rw [Order.lt_succ_iff] at ho
    obtain rfl | ho := ho.eq_or_lt
    exacts [⟨b, ha b hb, rfl⟩, IH _ hb ho]

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