English
There is a canonical bijection of the indexing set ι induced by reflection; this bijection is compatible with the maps sending roots to roots.
Русский
Существует каноническое биективное соответствие множества индексов ι, индуцируемое отражением; это биекция совместима с отображениями корней на корни.
LaTeX
$$$\\text{equiv\_of\_mapsTo} : ι \\to ι$ is a bijection with properties dictated by the reflected pairing.$$
Lean4
/-- The bijection on the indexing set induced by reflection. -/
@[simps]
protected def equiv_of_mapsTo : ι ≃ ι
where
toFun j := (exist_eq_reflection_of_mapsTo p root coroot i j h).choose
invFun j := (exist_eq_reflection_of_mapsTo p root coroot i j h).choose
left_inv j := choose_choose_eq_of_mapsTo p root coroot i j h hp
right_inv j := choose_choose_eq_of_mapsTo p root coroot i j h hp
