stabilizer_subset_div_right — Mathlib

English

If a ∈ s, then the stabilizer (as a set) is contained in the right quotient s / {a}.

Русский

Если a ∈ s, то стабилизатор ⊆ s / {a}.

LaTeX

$$$ (a \in s) \Rightarrow \uparrow(\operatorname{Stabilizer}_G(s)) \subseteq s / \{ a \} $$$

Lean4

@[to_additive]
theorem stabilizer_subset_div_right (ha : a ∈ s) : ↑(stabilizer G s) ⊆ s / { a } := fun b hb ↦
  ⟨_, by rwa [← smul_eq_mul, mem_stabilizer_set.1 hb], _, mem_singleton _, mul_div_cancel_right _ _⟩

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