prod_left_mono — Mathlib

English

The map that sends a sublattice L to L.prod M is monotone in its left argument.

Русский

Агрегат, которому отображение из подпределов в произведение с фиксированным правым аргументом, является монотонным по левому аргументу.

LaTeX

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

Lean4

theorem prod_left_mono : Monotone fun L : Sublattice α ↦ L.prod M := fun _ _ ↦ prod_mono_left

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