mul_subset_iff_right — Mathlib

English

Let s, t, u be finite sets in a semigroup with multiplication. Then the product s · t is contained in u if and only if for every b in t, the left translate of s by b, namely op(b) · s, is contained in u.

Русский

Пусть s, t, u — конечные множества в полугруппе с умножением. Тогда произведение s · t⊆u тогда и только если для каждого b ∈ t левая переноска s на b, то есть op(b) · s, содержится в u.

LaTeX

$$$s \\cdot t \\subseteq u \\;\\iff\\; \\forall b \\in t,\\; \\operatorname{op}(b) \\cdot s \\subseteq u$$$

Lean4

@[to_additive]
theorem mul_subset_iff_right : s * t ⊆ u ↔ ∀ b ∈ t, op b • s ⊆ u :=
  image₂_subset_iff_right

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