smul_subset_of_set_mem_fixedBy — Mathlib

English

If t ⊆ s and s ∈ fixedBy (Set α) g, then g • t ⊆ s.

Русский

Если t ⊆ s и s ∈ fixedBy (Set α) g, то g • t ⊆ s.

LaTeX

$$$ t \subseteq s \quad\Rightarrow\quad g \cdot t \subseteq s \quad\text{given } s \in fixedBy(Set α) g$$

Lean4

theorem smul_subset_of_set_mem_fixedBy {s t : Set α} {g : G} (t_ss_s : t ⊆ s) (s_in_fixedBy : s ∈ fixedBy (Set α) g) :
    g • t ⊆ s :=
  (Set.smul_set_subset_smul_set_iff.mpr t_ss_s).trans s_in_fixedBy.subset

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