le_pointwise_smul_iff₀

Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.le_pointwise_smul_iff₀

English

For a ≠ 0, S ≤ a · T is equivalent to a⁻¹ · S ≤ T.

Русский

Для a ≠ 0: S ≤ a · T ↔ a⁻¹ · S ≤ T.

LaTeX

$$$\forall a\neq 0:\ S,T:\text{AddSubmonoid } A:\ S \le a\cdot T\iff a^{-1}\cdot S \le T$.$$

Lean4

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

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

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

Разделы

Аффилиация

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