prod_mono_right — Mathlib

English

Let s be a subsemiring of R. For subsemirings t1, t2 of S, if t1 ≤ t2 then s.prod t1 ≤ s.prod t2. In words, the map t ↦ s.prod t is monotone with respect to inclusion.

Русский

Пусть s — подполусемиринг R. Для подполусемирингов t1, t2 S верно: если t1 ≤ t2, то s.prod t1 ≤ s.prod t2. Проще говоря, отображение t ↦ s.prod t монотонно по включениям.

LaTeX

$$$\\forall \\{t_1,t_2\\ :\\ Subsemiring\\ S\\},\\ t_1 \\le t_2\\ \\Rightarrow\\ s.prod\\ t_1 \\le s.prod\\ t_2$$$

Lean4

theorem prod_mono_right (s : Subsemiring R) : Monotone fun t : Subsemiring S => s.prod t :=
  prod_mono (le_refl s)

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