le_succ_rank_sUnion — Mathlib

English

The rank of the set x is bounded above by the successor of the rank of its sUnion.

Русский

Ранг множества x не превышает successors ранга ⋃₀ x.

LaTeX

$$$$ \operatorname{rank}(x) \le \operatorname{succ}(\operatorname{rank}(\bigcup x)) $$$$

Lean4

theorem le_succ_rank_sUnion (x : PSet) : rank x ≤ succ (rank (⋃₀ x)) :=
  by
  rw [← rank_powerset]
  apply rank_mono
  rw [subset_iff]
  intro z _
  rw [mem_powerset, subset_iff]
  intro _ _
  rw [mem_sUnion]
  exists z

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