pointwise_smul_le_pointwise_smul_iff

Mathlib.Algebra.Ring.Subsemiring.Pointwise

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

English

The relation between subset and smul: S ≤ a•T iff a⁻¹•S ≤ T.

Русский

Связь подмножеств и смула: S ≤ a•T эквивалентно a⁻¹•S ≤ T.

LaTeX

$$$S \le a \cdot T \iff a^{-1} \cdot S \le T$$$

Lean4

@[simp]
theorem pointwise_smul_le_pointwise_smul_iff {a : M} {S T : Subsemiring R} : a • S ≤ a • T ↔ S ≤ T :=
  smul_set_subset_smul_set_iff

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

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

Разделы

Аффилиация

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