English
Rank is equal to the well-founded rank with respect to membership.
Русский
Ранг равен WF-рангу по отношению принадлежности.
LaTeX
$$$$ \operatorname{lift}(\operatorname{rank} x) = \operatorname{IsWellFounded.rank}_{(\alpha := \mathrm{PSet})} (\;\cdot \in \cdot\,) x $$$$
Lean4
/-- `PSet.rank` is equal to the `IsWellFounded.rank` over `∈`. -/
theorem rank_eq_wfRank : lift.{u + 1, u} (rank x) = IsWellFounded.rank (α := PSet) (· ∈ ·) x :=
by
induction x using mem_wf.induction with
| _ x ih
rw [IsWellFounded.rank_eq]
simp_rw [← fun y : { y // y ∈ x } => ih y y.2]
apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _) <;> intro h
· rw [lt_lift_iff]
rintro ⟨o, h, rfl⟩
simpa [Ordinal.lt_iSup_iff] using lt_rank_iff.1 h
· simpa using rank_lt_of_mem h.2
