image_op_mul — Mathlib

English

Let s, t be subsets. Then the image under the opposite map of their product equals the product of the opposites in reverse order: op''(s · t) = op'' t · op'' s.

Русский

Пусть s, t — подмножества. Тогда образ их произведения в противоположной системе равен произведению образов в обратном порядке: op''(s · t) = op'' t · op'' s.

LaTeX

$$$\\operatorname{op}''(s \\cdot t) = \\operatorname{op}'' t \\cdot \\operatorname{op}'' s$$$

Lean4

@[to_additive (attr := simp)]
theorem image_op_mul : op '' (s * t) = op '' t * op '' s :=
  image_image2_antidistrib op_mul

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