replicate_le_replicate — Mathlib

English

For any a, k,n, replicate k a ≤ replicate n a iff k ≤ n.

Русский

Для любого a, k, n: replicate k a ≤ replicate n a тогда и только тогда, когда k ≤ n.

LaTeX

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

Lean4

theorem replicate_le_replicate (a : α) {k n : ℕ} : replicate k a ≤ replicate n a ↔ k ≤ n :=
  _root_.trans (by rw [← replicate_le_coe, coe_replicate]) (List.replicate_sublist_replicate a)

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