encard_diff_add_encard_inter

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

For sets S and T, (S \ T).encard + (S ∩ T).encard = S.encard.

Русский

Для множеств S и T выполняется (S \ T).encard + (S ∩ T).encard = S.encard.

LaTeX

$$$(S \ T).\encard + (S \cap T).\encard = S.\encard$$$

Lean4

theorem encard_diff_add_encard_inter (s t : Set α) : (s \ t).encard + (s ∩ t).encard = s.encard := by
  rw [← encard_union_eq (disjoint_of_subset_right inter_subset_right disjoint_sdiff_left), diff_union_inter]

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

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

Разделы

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

Аффилиация

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