pointwise_smul_le_pointwise_smul_iff

Mathlib.Algebra.GroupWithZero.Subgroup

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

English

For ha ≠ 0, a • S ≤ a • T ↔ S ≤ T.

Русский

Пусть ha ≠ 0. Тогда a • S ≤ a • T ↔ S ≤ T.

LaTeX

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

Lean4

@[simp]
theorem pointwise_smul_le_pointwise_smul_iff : a • S ≤ a • T ↔ S ≤ T :=
  smul_set_subset_smul_set_iff

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

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

Разделы

Аффилиация

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