star_mul — Mathlib

English

Star of a product equals the product of stars in reverse order: (s * t)⋆ = t⋆ * s⋆.

Русский

Звезда произведения равна произведению звезд в обратном порядке: (s * t)⋆ = t⋆ * s⋆.

LaTeX

$$$ (s \\cdot t)^{\\star} = t^{\\star} \\cdot s^{\\star}. $$$

Lean4

protected theorem star_mul [Mul α] [StarMul α] (s t : Set α) : (s * t)⋆ = t⋆ * s⋆ := by
  simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right, star_mul, image2_swap _ s t]

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