inv_op_smul_set_distrib₀ — Mathlib

English

For any a, s ⊆ α, the inverse of the left-acted set distributes with op-scalar: (s <• a)⁻¹ = a⁻¹ • s⁻¹.

Русский

Для любого a, s ⊆ α, обратное от левого действия набора распределяется как a⁻¹ • s⁻¹.

LaTeX

$$$ (s <\cdot a)^{-1} = a^{-1} \cdot s^{-1} $$$

Lean4

@[simp]
theorem inv_op_smul_set_distrib₀ (a : α) (s : Set α) : (s <• a)⁻¹ = a⁻¹ • s⁻¹ :=
  by
  obtain rfl | ha := eq_or_ne a 0
  · obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]
  · ext; simp [mem_smul_set_iff_inv_smul_mem₀, *]

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