rank_sUnion_le — Mathlib

English

The rank of the sUnion of x does not exceed the rank of x.

Русский

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

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 : PSet) : rank (⋃₀ x) ≤ rank x :=
  by
  simp_rw [rank_le_iff, mem_sUnion]
  intro _ ⟨_, _, _⟩
  trans <;> apply rank_lt_of_mem <;> assumption

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