image_op_inv — Mathlib

English

The image under the opposite map of the inverse of a set equals the inverse of the image under the opposite map.

Русский

Образ под операцией противоположности от обратного множества равен обратному образу под противоположностью.

LaTeX

$$$ \operatorname{op} '' s^{-1} = (\operatorname{op} '' s)^{-1} $$$

Lean4

@[to_additive]
theorem image_op_inv : op '' s⁻¹ = (op '' s)⁻¹ := by simp_rw [← image_inv_eq_inv, Function.Semiconj.set_image op_inv s]

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