prod_mono_left

Mathlib.RingTheory.NonUnitalSubring.Basic

URI: https://scilib.ai/kg/mathlib#NonUnitalSubring.prod_mono_left

English

The map s ↦ s.prod t is monotone.

Русский

Отображение s ↦ s.prod t монотонно по включению.

LaTeX

$$$\text{Monotone}(\lambda s, s.prod t)$$$

Lean4

theorem prod_mono_left (t : NonUnitalSubring S) : Monotone fun s : NonUnitalSubring R => s.prod t := fun _s₁ _s₂ hs =>
  prod_mono hs (le_refl t)

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

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

Разделы

Аффилиация

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