pointwise_smul_le_iff₀

Mathlib.Algebra.GroupWithZero.Subgroup

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

English

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

Русский

Для ha ≠ 0 выполняется S ≤ a • T ⇔ a⁻¹ • S ≤ T.

LaTeX

$$$ (ha \neq 0) \\\\Rightarrow \\\\ S \\le a \\cdot T \\\\iff \\\\ a^{-1} \\cdot S \\le T $$$

Lean4

theorem pointwise_smul_le_iff₀ (ha : a ≠ 0) : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
  smul_set_subset_iff₀ ha

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

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

Разделы

Аффилиация

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