dens_sdiff

Mathlib.Data.Finset.Density

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

English

For Finsets s,t, dens t − dens s ≤ dens(t \\ s).

Русский

Для Finset s,t верно dens(t) − dens(s) ≤ dens(t \\ s).

LaTeX

$$$ \\operatorname{dens}(t) - \\operatorname{dens}(s) \\leq \\operatorname{dens}(t \\setminus s) $$$

Lean4

theorem dens_sdiff (h : s ⊆ t) : dens (t \ s) = dens t - dens s :=
  eq_tsub_of_add_eq (dens_sdiff_add_dens_eq_dens h)

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

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

Разделы

Аффилиация

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