English
If a derivation D lies in the Killing orthogonal of the range of the adjoint action, then for every x in L, ad(D x) also lies in this Killing orthogonal.
Русский
Пусть D — вывод derivation, принадлежащий Killing-ортогональности диапазона линейного отображения сопряженного действия, тогда для любого x∈L выполняется ad(Dx) ∈ Killing-ортогональность.
LaTeX
$$$\forall R\, \forall L\,[Field\ R]\,[LieRing\ L]\,[LieAlgebra\ R\ L], \forall {D : LieDerivation\ R\ L\ L},\ D \in 𝕀^\perp \Rightarrow (\forall x \in L\, ad_{R,L}(D x) \in 𝕀^\perp).$$$
Lean4
/-- If a derivation `D` is in the Killing orthogonal of the range of the adjoint action, then, for
any `x : L`, `ad (D x)` is also in this orthogonal. -/
theorem ad_mem_orthogonal_of_mem_orthogonal {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) : ad R L (D x) ∈ 𝕀ᗮ :=
by
simp only [ad_apply_lieDerivation, LieHom.range_toSubmodule, neg_mem_iff]
exact (rangeAdOrthogonal R L).lie_mem hD
