mem_smul — Mathlib

English

An element x belongs to s • t if and only if 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 \cdot t \iff \exists y \in s, \exists z \in t, y \cdot z = x $$$

Lean4

@[to_additive]
theorem mem_smul {x : β} : x ∈ s • t ↔ ∃ y ∈ s, ∃ z ∈ t, y • z = x :=
  mem_image₂

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