encard_diff_add_encard_of_subset

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

If S ⊆ T, then (T \ S).encard + S.encard = T.encard.

Русский

Если S ⊆ T, тогда encard(T \ S) + encard(S) = encard(T).

LaTeX

$$$S \subseteq T \Rightarrow (T \setminus S).\encard + S.\encard = T.\encard$$$

Lean4

theorem encard_diff_add_encard_of_subset (h : s ⊆ t) : (t \ s).encard + s.encard = t.encard := by
  rw [← encard_union_eq disjoint_sdiff_left, diff_union_self, union_eq_self_of_subset_right h]

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

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

Разделы

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

Аффилиация

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