mulRightMono

Mathlib.Data.Set.Semiring

URI: https://scilib.ai/kg/mathlib#SetSemiring.mulRightMono

English

Multiplication is monotone in the right argument: if s ⊆ t then u * s ⊆ u * t.

Русский

Умножение монотонно по правому аргументу: если s ⊆ t, то u * s ⊆ u * t.

LaTeX

$$s \subseteq t \Rightarrow u * s \subseteq u * t$$

Lean4

instance mulRightMono : MulRightMono (SetSemiring α) :=
  ⟨fun _ _ _ => mul_subset_mul_right⟩

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

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

Разделы

Аффилиация

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