subset_conjugatesOfSet — Mathlib

English

Let s ⊆ t be subsets of a group. Then the conjugates of s are contained in the conjugates of t.

Русский

Пусть s ⊆ t — подмножества группы. Тогда конъюгаты s содержатся в конъюгатах t.

LaTeX

$$$ s \subseteq t \Rightarrow \mathrm{conjugatesOfSet}(s) \subseteq \mathrm{conjugatesOfSet}(t) $$$

Lean4

theorem subset_conjugatesOfSet : s ⊆ conjugatesOfSet s := fun (x : G) (h : x ∈ s) =>
  mem_conjugatesOfSet_iff.2 ⟨x, h, IsConj.refl _⟩

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