tsub_encard_le_encard_diff — Mathlib

English

For any sets S and T, the EN-cardinality satisfies encard(S) − encard(T) ≤ encard(S ∖ T).

Русский

Для любых множеств S и T выполняется неравенство encard(S) − encard(T) ≤ encard(S \setminus T).

LaTeX

$$$encard(s) - encard(t) \\le encard(s \\setminus t)$$$

Lean4

theorem tsub_encard_le_encard_diff (s t : Set α) : s.encard - t.encard ≤ (s \ t).encard := by
  rw [tsub_le_iff_left, add_comm]; apply encard_le_encard_diff_add_encard

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