eq_replicate_length — Mathlib

English

For any a and l, l equals replicate(l.length, a) if and only if every element of l equals a.

Русский

Для любого элемента a и списка l справедливо: l = replicate(l.length, a) тогда и только тогда, когда каждый элемент l равен a.

LaTeX

$$$$\\forall a:\\\\alpha,\\\\forall l:\\\\mathrm{List}\\\\alpha,\\ l = \\mathrm{replicate}(l.length, a) \\\\iff \\\\forall b \\in l,\\\\ b = a.$$$$

Lean4

theorem eq_replicate_length {a : α} : ∀ {l : List α}, l = replicate l.length a ↔ ∀ b ∈ l, b = a
  | [] => by simp
  | (b :: l) => by simp [eq_replicate_length, replicate_succ]

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