card_union_le — Mathlib

English

For sets s,t ⊆ α, Nat.card (s ∪ t) ≤ Nat.card s + Nat.card t.

Русский

Для множеств s,t ⊆ α выполняется: card( s ∪ t ) ≤ card(s) + card(t).

LaTeX

$$$Nat.card(\uparrow(s \cup t)) \le Nat.card(s) + Nat.card(t)$$$

Lean4

theorem card_union_le (s t : Set α) : Nat.card (↥(s ∪ t)) ≤ Nat.card s + Nat.card t :=
  by
  rcases _root_.finite_or_infinite (↥(s ∪ t)) with h | h
  · rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h
    cases h
    rw [← @Nat.cast_le Cardinal, Nat.cast_add, Nat.cast_card, Nat.cast_card, Nat.cast_card]
    exact Cardinal.mk_union_le s t
  · exact Nat.card_eq_zero_of_infinite.trans_le (zero_le _)

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