isChain_eq_iff_eq_replicate — Mathlib

English

A list l is a chain under equality if and only if every element of l equals a common value a; equivalently, l = replicate (length l) a for some a.

Русский

Список l является цепью по отношению равенства тогда и только тогда, когда все элементы равны одному общему значению a; эквивалентно l = replicate (длину l) a.

LaTeX

$$$IsChain(=)\\ l\\iff \\exists a:\\alpha,\\ l=head? \\, a\\land\\ l= Replicate(|l|)\\ a$$$

Lean4

theorem isChain_eq_iff_eq_replicate {l : List α} : IsChain (· = ·) l ↔ ∀ a ∈ l.head?, l = replicate l.length a := by
  induction l using twoStepInduction with
  | nil
  | singleton => simp
  | cons_cons a b l IH IH2 => simp +contextual [isChain_cons_cons, eq_comm, IH2, replicate_succ]

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