pointwise_smul_le_pointwise_smul_iff

Mathlib.Algebra.Group.Subgroup.Pointwise

URI: https://scilib.ai/kg/mathlib#Subgroup.pointwise_smul_le_pointwise_smul_iff

English

For a ∈ α and subgroups S, T of G, a · S ≤ T if and only if S ≤ a⁻¹ · T.

Русский

Для a ∈ α и подгрупп S, T в G верно: a · S ≤ T тогда и только тогда, когда S ≤ a⁻¹ · T.

LaTeX

$$$ a \cdot S \le T \iff S \le a^{-1} \cdot T $$$

Lean4

@[simp]
theorem pointwise_smul_le_pointwise_smul_iff {a : α} {S T : Subgroup G} : a • S ≤ a • T ↔ S ≤ T :=
  smul_set_subset_smul_set_iff

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

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

Разделы

Аффилиация

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