pointwise_smul_le_pointwise_smul_iff₀

Mathlib.Algebra.GroupWithZero.Subgroup

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

English

If ha ≠ 0, then a • S ≤ a • T iff S ≤ T.

Русский

Пусть ha ≠ 0. Тогда a • S ≤ a • T эквивалентно S ≤ T.

LaTeX

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

Lean4

@[simp]
theorem pointwise_smul_le_pointwise_smul_iff₀ (ha : a ≠ 0) : a • S ≤ a • T ↔ S ≤ T :=
  smul_set_subset_smul_set_iff₀ ha

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

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

Разделы

Аффилиация

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