op_smul_coe_set — Mathlib

English

Left action by MulOpposite.op a on the underlying set of S yields S if a ∈ S.

Русский

Левое действие MulOpposite.op a на множество S даёт S, если a ∈ S.

LaTeX

$$MulOpposite.op a • (S : Set G) = S при a ∈ S$$

Lean4

@[to_additive (attr := simp)]
theorem op_smul_coe_set [Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
    MulOpposite.op a • (s : Set G) = s := by ext; simp [Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_right, ha]

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