rank_union — Mathlib

English

For ZF sets x,y, the rank of their union x ∪ y is the maximum of their ranks.

Русский

Ранг объединения x ∪ y равен максимуму рангов x и y.

LaTeX

$$$$ \operatorname{rank}(x \cup y) = \max( \operatorname{rank} x, \operatorname{rank} y) $$$$

Lean4

@[simp]
theorem rank_union (x y : ZFSet) : rank (x ∪ y) = max (rank x) (rank y) :=
  by
  apply le_antisymm
  · simp_rw [rank_le_iff, mem_union, lt_max_iff]
    intro
    apply Or.imp <;> apply rank_lt_of_mem
  · apply max_le <;> apply rank_mono <;> intro _ h <;> simp [h]

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