mulSingle_strictMono

Mathlib.Algebra.Group.Pi.Lemmas

URI: https://scilib.ai/kg/mathlib#Pi.mulSingle_strictMono

English

For a fixed index i, the map Pi.mulSingle i is strictly monotone with respect to the preorder on f i.

Русский

Для фиксированного индекса i отображение Pi.mulSingle i строго монотонно по предпорядку на f i.

LaTeX

$$$\mathrm{StrictMono}(\mathrm{Pi.mulSingle}_i)$$$

Lean4

@[to_additive]
theorem mulSingle_strictMono : StrictMono (Pi.mulSingle i : f i → ∀ i, f i) :=
  Function.update_strictMono

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

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

Разделы

Аффилиация

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