rank_sUnion_le — Mathlib

English

For ZF sets, the rank of the sUnion is bounded above by the rank of the original set.

Русский

Ранг ⋃₀ x не превосходит ранга x в ZFSet.

LaTeX

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

Lean4

/-- For the rank of `⋃₀ x`, we only have `rank (⋃₀ x) ≤ rank x ≤ rank (⋃₀ x) + 1`.

This inequality is split into `rank_sUnion_le` and `le_succ_rank_sUnion`. -/
theorem rank_sUnion_le (x : ZFSet) : rank (⋃₀ x) ≤ rank x :=
  by
  simp_rw [rank_le_iff, mem_sUnion]
  intro _ ⟨_, _, _⟩
  trans <;> apply rank_lt_of_mem <;> assumption

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