mem_mul — Mathlib

English

An element x lies in the product p*q exactly when x can be written as a product y*z with y ∈ p and z ∈ q.

Русский

Элемент x принадлежит произведению p*q тогда и только тогда, когда x можно записать как y·z с y ∈ p и z ∈ q.

LaTeX

$$$x \\in p * q \\iff \\exists y \\in p, \\exists z \\in q, y * z = x.$$$

Lean4

theorem mem_mul {p q : SubMulAction R M} {x : M} : x ∈ p * q ↔ ∃ y ∈ p, ∃ z ∈ q, y * z = x :=
  Set.mem_mul

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