card_inv_le

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

The size of the inverse Finset is at most the size of the original: |s⁻¹| ≤ |s|.

Русский

Размер s⁻¹ не превосходит размера s: |s⁻¹| ≤ |s|.

LaTeX

$$$ \#s^{-1} \leq \#s $$$

Lean4

@[to_additive]
theorem card_inv_le : #s⁻¹ ≤ #s :=
  card_image_le

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

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

Разделы

Аффилиация

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