mem_range_rank_of_le — Mathlib

English

Given Acc r a and o ≤ rank r a, there is b with Acc r b and rank r b = o.

Русский

С учетом Acc r a и o ≤ rank r a, существует b с Acc r b и rank r b = o.

LaTeX

$${o : Ordinal} (ha : Acc r a) (ho : o ≤ ha.rank) → ∃ b, hb : Acc r b, hb.rank = o$$

Lean4

theorem mem_range_rank_of_le {o : Ordinal} (h : o ≤ rank r a) : o ∈ Set.range (rank r) :=
  by
  obtain ⟨b, hb, rfl⟩ := Acc.mem_range_rank_of_le (hwf.apply r a) h
  exact ⟨b, rfl⟩

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