instCovariantClassHSMulLe

Mathlib.Algebra.Ring.Subring.Pointwise

URI: https://scilib.ai/kg/mathlib#Subring.instCovariantClassHSMulLe

English

The action of M on Subring R is monotone with respect to inclusion: a • S ≤ a • T whenever S ≤ T.

Русский

Действие M на Subring R монотонно по включениям: если S ⊆ T, то a • S ⊆ a • T.

LaTeX

$$$\forall a \in M, \forall S,T \subseteq R,\ S \le T \Rightarrow a \cdot S \le a \cdot T$$$

Lean4

instance : CovariantClass M (Subring R) HSMul.hSMul LE.le :=
  ⟨fun _ _ => image_mono⟩

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

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

Разделы

Аффилиация

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