rank_powerset — Mathlib

English

The rank of the powerset of x is the successor of rank x.

Русский

Ранг множества мощности над x равен следующему рангу x.

LaTeX

$$$$ \operatorname{rank}(\mathcal{P}(x)) = \operatorname{succ}(\operatorname{rank}(x)) $$$$

Lean4

@[simp]
theorem rank_powerset (x : PSet) : rank (powerset x) = succ (rank x) :=
  by
  apply le_antisymm
  · simp_rw [rank_le_iff, mem_powerset, lt_succ_iff]
    intro
    exact rank_mono
  · rw [succ_le_iff]
    apply rank_lt_of_mem
    simp

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