mul_le

Mathlib.Algebra.Ring.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.mul_le

English

M N ≤ P iff ∀ m ∈ M, ∀ n ∈ N, m n ∈ P.

Русский

M N ≤ P тогда и только тогда, когда для любых m ∈ M и n ∈ N выполняется m n ∈ P.

LaTeX

$$$M * N \le P \iff \forall m \in M, \forall n \in N, m n \in P$$$

Lean4

theorem mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P :=
  smul_le

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

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

Разделы

Аффилиация

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