rank_insert — Mathlib

English

Let x and y be ZFSet. The rank of the set obtained by inserting x into y is the maximum of succ(rank x) and rank y.

Русский

Пусть x и y — ZFSet. Ранг множества, полученного вставкой x в y, равен максимуму succ(rank x) и rank y.

LaTeX

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

Lean4

@[simp]
theorem rank_insert (x y : ZFSet) : rank (insert x y) = max (succ (rank x)) (rank y) :=
  Quotient.inductionOn₂ x y PSet.rank_insert

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