ofFixingSubgroup_insert_map_bijective

English

The map between fixingSubgroups is bijective.

Русский

Отображение между фиксирующими подгруппами биективно.

LaTeX

$$$Bijective\ (ofFixingSubgroup\insert\_map\ a\ s)$$$

Lean4

@[to_additive]
theorem ofFixingSubgroup_insert_map_bijective {a : α} {s : Set (ofStabilizer M a)} :
    Bijective (ofFixingSubgroup_insert_map a s) := by
  constructor
  · rintro ⟨x, hx⟩ ⟨y, hy⟩ h
    simpa only [← Subtype.coe_inj, ofFixingSubgroup_insert_map_apply] using h
  · rintro ⟨⟨x, hx1⟩, hx2⟩
    exact ⟨⟨x, mem_ofFixingSubgroup_insert_iff.mpr ⟨hx1, hx2⟩⟩, rfl⟩

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