rank_pair — Mathlib

English

For PSets x,y, the rank of the set {x,y} is 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 : PSet) : rank { x, y } = max (succ (rank x)) (succ (rank y)) := by simp

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