dens_inv

Mathlib.Algebra.Group.Pointwise.Finset.Density

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

English

The density of a set is invariant under taking inverse: dens(s⁻¹) = dens(s).

Русский

Плотность множества сохраняется при взятии обратного: dens(S⁻¹) = dens(S).

LaTeX

$$$\text{dens}(s^{-1}) = \text{dens}(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem dens_inv [Fintype α] (s : Finset α) : s⁻¹.dens = s.dens := by simp [dens]

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

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

Разделы

Аффилиация

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