op_smul_set_stabilizer_subset — Mathlib

English

If a ∈ s, then the op-Smul of the stabilizer by a is contained in s.

Русский

Если a ∈ s, то op-умножение стабилизатора на a подчёркнуто лежит в s.

LaTeX

$$$ (a ∈ s) \Rightarrow (\operatorname{Stab}_G(s))^{\mathrm{op}} \cdot a \subseteq s $$$

Lean4

@[to_additive]
theorem op_smul_set_stabilizer_subset (ha : a ∈ s) : (stabilizer G s : Set G) <• a ⊆ s :=
  smul_set_subset_iff.2 fun b hb ↦ by rw [← hb]; exact smul_mem_smul_set ha

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