prod_right_mono

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.prod_right_mono

English

The map M ↦ L.prod M is monotone in its right argument.

Русский

Отображение M ↦ L.prod M монотонно по правому аргументу.

LaTeX

$$Monotone(M \\mapsto L \\prod M)$$

Lean4

theorem prod_right_mono : Monotone fun M : Sublattice β ↦ L.prod M := fun _ _ ↦ prod_mono_right

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

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

Разделы

Аффилиация

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