conjugatesOfSet_mono

Mathlib.Algebra.Group.Subgroup.Basic

URI: https://scilib.ai/kg/mathlib#Group.conjugatesOfSet_mono

English

The operation of taking conjugates of a set is monotone with respect to inclusion.

Русский

Операция взятия конъюгатов множества монотонна по включению.

LaTeX

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

Lean4

theorem conjugatesOfSet_mono {s t : Set G} (h : s ⊆ t) : conjugatesOfSet s ⊆ conjugatesOfSet t :=
  Set.biUnion_subset_biUnion_left h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru