pointwise_smul_le_pointwise_smul_iff

English

Let a be a group element; a • S ≤ a • T is equivalent to S ≤ T when S, T are AddSubmonoids and the action is by a central scalar.

Русский

Пусть a — элемент группы; a • S ≤ a • T эквивалентно S ≤ T при условии, что S, T — AddSubmonoid и действие задан центральным скаляром.

LaTeX

$$$ (a \neq 0) \Rightarrow (a \cdot S \le a \cdot T \iff S \le T) $$$

Lean4

@[simp]
theorem pointwise_smul_le_pointwise_smul_iff {S T : AddSubmonoid A} : a • S ≤ a • T ↔ S ≤ T :=
  smul_set_subset_smul_set_iff

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