instMulLeftMono

Mathlib.Algebra.Group.Pointwise.Set.Basic

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

English

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

Русский

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

LaTeX

$$∀ s t_1 t_2, t_1 ⊆ t_2 → s * t_1 ⊆ s * t_2$$

Lean4

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

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

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

Разделы

Аффилиация

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