dens_sdiff_add_dens

Mathlib.Data.Finset.Density

URI: https://scilib.ai/kg/mathlib#Finset.dens_sdiff_add_dens

← MathLib Explorer

English

For all s,t, dens(t \\ s) + dens(s) = dens(t ∪ s).

Русский

Для всех s,t: dens(t \\ s) + dens(s) = dens(t ∪ s).

LaTeX

$$$ \\operatorname{dens}(t \\ s) + \\operatorname{dens}(s) = \\operatorname{dens}(t \\cup s) $$$

Lean4

theorem dens_sdiff_add_dens (s t : Finset α) : dens (s \ t) + dens t = (s ∪ t).dens := by
  rw [← dens_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]

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

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

Разделы

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

Аффилиация

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