le_mk_diff_add_mk — Mathlib

English

Let S and T be subsets of a type. Then the cardinality of S is at most the sum of the cardinalities of S \\ T and T: |S| ≤ |S \\ T| + |T|.

Русский

Пусть S и T — подмножества множества; тогда кардинал множества S не превышает сумму кардиналов множеств S \\ T и T: |S| ≤ |S \\ T| + |T|.

LaTeX

$$$|S| \\le |S \\setminus T| + |T|$$$

Lean4

theorem le_mk_diff_add_mk (S T : Set α) : #S ≤ #(S \ T : Set α) + #T :=
  (mk_le_mk_of_subset <| subset_diff_union _ _).trans <| mk_union_le _ _

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