ncard_union_le — Mathlib

English

For any sets s,t, the cardinality of their union is at most the sum of their cardinalities: |s ∪ t| ≤ |s| + |t|.

Русский

Для любых множеств s и t справедливо: |s ∪ t| ≤ |s| + |t|.

LaTeX

$$$$ |s \cup t| \le |s| + |t| $$$$

Lean4

theorem ncard_union_le (s t : Set α) : (s ∪ t).ncard ≤ s.ncard + t.ncard :=
  by
  obtain (h | h) := (s ∪ t).finite_or_infinite
  · to_encard_tac
    rw [h.cast_ncard_eq, (h.subset subset_union_left).cast_ncard_eq, (h.subset subset_union_right).cast_ncard_eq]
    apply encard_union_le
  rw [h.ncard]
  apply zero_le

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