image_inv_eq_inv

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

The image under inversion distributes over Finset: image (·⁻¹) s = s⁻¹.

Русский

Изображение инверсии распределено над Finset: image (x ↦ x⁻¹) s = s⁻¹.

LaTeX

$$$ \mathrm{image}(\lambda x. x^{-1}, s) = s^{-1} $$$

Lean4

@[to_additive]
theorem image_inv_eq_inv (s : Finset α) : s.image (·⁻¹) = s⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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