pair_mul — Mathlib

English

The product s * {a,b} equals s transformed by a and s transformed by b, unioned.

Русский

Произведение s и {a,b} равно объединению a-трансформаций s и b-трансформаций s.

LaTeX

$$$ s * \{a,b\} = s \;\mathbf{•}_a \;\cup\; s \;\mathbf{•}_b $$$

Lean4

@[to_additive]
theorem pair_mul (a b : α) (s : Set α) : { a, b } * s = a • s ∪ b • s := by
  rw [insert_eq, union_mul, singleton_mul, singleton_mul]; rfl

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