mapsTo_reflection_root — Mathlib

English

Let P be a RootPairing on ι with root map root. Then for every i, the reflection map associated to i sends every root to a root, i.e., the root set is invariant under the reflection.

Русский

Пусть P задаёт систему корней на индексе ι и отображение корня root. Тогда для каждого i отображение отражения, связанное с i, отправляет любой корень в другой корень; множество корней инвариантно относительно этого отражения.

LaTeX

$$$ (P.reflection(i))\' (range(P.root)) \subseteq range(P.root) $$$

Lean4

theorem mapsTo_reflection_root : MapsTo (P.reflection i) (range P.root) (range P.root) :=
  by
  rintro - ⟨j, rfl⟩
  exact P.root_reflectionPerm i j ▸ mem_range_self (P.reflectionPerm i j)

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