English
Let x and y be PSets. The rank of the set obtained by inserting x into y equals the maximum of succ(rank x) and rank y.
Русский
Пусть x и y — множества-подмножества. Ранг множества, полученного добавлением 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 : PSet) : rank (insert x y) = max (succ (rank x)) (rank y) :=
by
apply le_antisymm
· simp_rw [rank_le_iff, mem_insert_iff]
rintro _ (h | h)
· simp [rank_congr h]
· simp [rank_lt_of_mem h]
· apply max_le
· exact (rank_lt_of_mem (mem_insert x y)).succ_le
· exact rank_mono (subset_iff.2 fun z => mem_insert_of_mem x)
