ofFixingSubgroup_equivariantMap_injective

English

The equivariant identity map from fixingSubgroup M s into α is injective.

Русский

Эквивариантное отображение-идентичность из fixingSubgroup M s в α инъективно.

LaTeX

$$$\operatorname{Injective}\bigl(ofFixingSubgroup\\_equivariantMap\ M\ s\\bigr).$$$

Lean4

@[to_additive]
theorem ofFixingSubgroup_equivariantMap_injective : Injective (ofFixingSubgroup_equivariantMap M s) :=
  by
  rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
  simpa [Subtype.mk.injEq] using hxy

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