encard_le_encard_diff_add_encard

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.encard_le_encard_diff_add_encard

← MathLib Explorer

English

For any S, T, encard(S) ≤ encard((S \ T)) + encard(T).

Русский

Для любых S, T выполняется encard(S) ≤ encard(S \ T) + encard(T).

LaTeX

$$$\operatorname{encard}(S) \le \operatorname{encard}(S \setminus T) + \operatorname{encard}(T)$$$

Lean4

theorem encard_le_encard_diff_add_encard (s t : Set α) : s.encard ≤ (s \ t).encard + t.encard :=
  (encard_mono subset_union_left).trans_eq (encard_diff_add_encard _ _).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru