conjMap_bijective — Mathlib

English

The conjugation map conjMap hg is a bijection between the relevant stabilizers.

Русский

Отображение conjMap hg является биекцией между соответствующими стабилизаторами.

LaTeX

$$$\\operatorname{Bijective}(\\mathrm{conjMap}_{hg}).$$$

Lean4

@[to_additive]
theorem conjMap_bijective : Function.Bijective (conjMap hg) :=
  by
  constructor
  · rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
    simp only [Subtype.mk_eq_mk]
    apply (MulAction.injective g)
    rwa [← SetLike.coe_eq_coe, conjMap_apply] at hxy
  · intro x
    exact ⟨conjMap _ x, inv_conjMap_comp_apply _ x⟩

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