le_dens_sdiff

Mathlib.Data.Finset.Density

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

English

The same inequality as above, expressed with left density.

Русский

Та же неравенство слева для плотности разности.

LaTeX

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

Lean4

theorem le_dens_sdiff (s t : Finset α) : dens t - dens s ≤ dens (t \ s) :=
  tsub_le_iff_right.2 dens_le_dens_sdiff_add_dens

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

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

Разделы

Аффилиация

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