English
Rank is monotone with respect to inclusion: if x ⊆ y, then rank x ≤ rank y.
Русский
Ранг монотонен по включению: если x ⊆ y, то rank x ≤ rank y.
LaTeX
$$$$ \text{If } x \subseteq y, \quad \operatorname{rank}(x) \le \operatorname{rank}(y) $$$$
Lean4
/-- `ZFSet.rank` is equal to the `IsWellFounded.rank` over `∈`. -/
theorem rank_eq_wfRank : lift.{u + 1, u} (rank x) = IsWellFounded.rank (α := ZFSet) (· ∈ ·) x :=
by
induction x using inductionOn 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
