mem_normalizer_iff — Mathlib

English

For a LieSubalgebra H and x ∈ L, x ∈ H.normalizer iff ∀ y ∈ H, [x,y] ∈ H.

Русский

Для подалгебры H и элемента x ∈ L верно: x ∈ H.normalizer тогда и только тогда, когда ∀ y ∈ H, [x,y] ∈ H.

LaTeX

$$$ x \\in H.normalizer \\iff \\forall y : L, y \\in H \\rightarrow [x,y] \\in H $$$

Lean4

theorem mem_normalizer_iff (x : L) : x ∈ H.normalizer ↔ ∀ y : L, y ∈ H → ⁅x, y⁆ ∈ H :=
  by
  rw [mem_normalizer_iff']
  refine forall₂_congr fun y hy => ?_
  rw [← lie_skew, neg_mem_iff (G := L)]

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