English
If S ⊆ G is finite and x ∈ G satisfies that x n x^{-1} ∈ S for all n ∈ S, then x ∈ Normalizer(S).
Русский
Если S ⊆ G конечно, и xn x^{-1} ∈ S для всех n ∈ S, то x ∈ нормализатора S.
LaTeX
$$$x\in \mathrm{setNormalizer}(S)$ under the given finiteness and conjugation-closure conditions$$
Lean4
theorem mem_normalizer_fintype {S : Set G} [Finite S] {x : G} (h : ∀ n, n ∈ S → x * n * x⁻¹ ∈ S) :
x ∈ Subgroup.setNormalizer S := by
haveI := Classical.propDecidable; cases nonempty_fintype S
exact fun n =>
⟨h n, fun h₁ =>
have heq : (fun n => x * n * x⁻¹) '' S = S :=
Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
(by rw [Set.card_image_of_injective S conj_injective])
have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
let ⟨y, hy⟩ := this
conj_injective hy.2 ▸ hy.1⟩
