rank_pair — Mathlib

English

For ZF sets x,y, the rank of the pair {x,y} equals the maximum of succ(rank x) and succ(rank y).

Русский

Для множеств x и y ранг множества {x,y} равен максимуму между succ(rank x) и succ(rank y).

LaTeX

$$$$ \operatorname{rank}(\{ x, y \}) = \max\big( \operatorname{succ}(\operatorname{rank} x), \operatorname{succ}(\operatorname{rank} y) \big) $$$$

Lean4

theorem rank_pair (x y : ZFSet) : rank { x, y } = max (succ (rank x)) (succ (rank y)) := by simp

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