mem_mul

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

An element x belongs to s*t iff there exist y ∈ s and z ∈ t with y*z = x.

Русский

Элемент x принадлежит s*t тогда и только тогда, когда существуют y ∈ s и z ∈ t такие, что y*z = x.

LaTeX

$$$x \in s * t \iff \exists y \in s, \exists z \in t, y \cdot z = x$$$

Lean4

@[to_additive]
theorem mem_mul {x : α} : x ∈ s * t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x :=
  mem_image₂

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

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

Разделы

Аффилиация

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