replicate_mono

Mathlib.Data.Multiset.Replicate

URI: https://scilib.ai/kg/mathlib#Multiset.replicate_mono

English

If k ≤ n then replicate k a ≤ replicate n a.

Русский

Если k ≤ n, то replicate k a ≤ replicate n a.

LaTeX

$$$k \\le n \\Rightarrow \\operatorname{replicate}(k,a) \\le \\operatorname{replicate}(n,a)$$$

Lean4

@[gcongr]
theorem replicate_mono (a : α) {k n : ℕ} (h : k ≤ n) : replicate k a ≤ replicate n a :=
  (replicate_le_replicate a).2 h

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

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

Разделы

Аффилиация

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