mem_inv

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

For a Finset s with an inversion on α, an element x belongs to s⁻¹ iff there exists y ∈ s with y⁻¹ = x.

Русский

Для Finset s с инверсией: x ∈ s⁻¹ тогда и только тогда, когда существует y ∈ s такое, что y⁻¹ = x.

LaTeX

$$$ x \in s^{-1} \iff \exists y \in s, y^{-1} = x $$$

Lean4

@[to_additive]
theorem mem_inv {x : α} : x ∈ s⁻¹ ↔ ∃ y ∈ s, y⁻¹ = x :=
  mem_image

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

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

Разделы

Аффилиация

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