instMulRightMono

Mathlib.Algebra.Group.Pointwise.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.instMulRightMono

English

For fixed t, the map s ↦ s * t is order-preserving: if s₁ ⊆ s₂ then s₁ * t ⊆ s₂ * t.

Русский

Для фиксированного t отображение s ↦ s * t сохраняет порядок: если s₁ ⊆ s₂, то s₁ * t ⊆ s₂ * t.

LaTeX

$$∀ s t_1 t_2, s_1 ⊆ s_2 → s_1 * t ⊆ s_2 * t$$

Lean4

@[to_additive]
instance : MulRightMono (Set α) where elim _t _s₁ _s₂ := mul_subset_mul_right

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

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

Разделы

Аффилиация

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