ofFixingSubgroup_insert_map_apply

English

The map application on a fixed element equals the element itself.

Русский

Применение отображения к фиксированному элементу даёт этот же элемент.

LaTeX

$$$(ofFixingSubgroupInsertMap\ a\ s)\ x = x$$$

Lean4

@[to_additive (attr := simp)]
theorem ofFixingSubgroup_insert_map_apply {a : α} {s : Set (ofStabilizer M a)} {x : α}
    (hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))) : (ofFixingSubgroup_insert_map a s) ⟨x, hx⟩ = x :=
  rfl

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