ofFixingSubgroup_of_inclusion_injective

English

If t is a subset of s, the natural inclusion map from the fixing-subgroup of t to the fixing-subgroup of s is injective.

Русский

Пусть t ⊆ s. Натуральное вложение фиксационной подгруппы t в фиксационную подгруппу s является инъективным.

LaTeX

$$$\operatorname{Injective}\big(\mathrm{ofFixingSubgroup\_of\_inclusion}(M,hst)\big)$$$

Lean4

@[to_additive]
theorem ofFixingSubgroup_of_inclusion_injective {hst : t ⊆ s} : Injective (ofFixingSubgroup_of_inclusion M hst) :=
  by
  rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
  rw [← SetLike.coe_eq_coe] at hxy ⊢
  exact hxy

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