getLast?_flatten_replicate — Mathlib

English

For any nonzero n, the last element option of the flatten of replicate n of l equals the last element option of l.

Русский

Для любого n ≠ 0 последняя опциональная величина после расплющивания повторов равна последней опциональной величине l.

LaTeX

$$$$\\forall n:\\\\mathbb{N},\\\\ n \\neq 0 \\\\to \\\\forall l:\\\\mathrm{List}\\\\alpha,\n\\\\ List.getLast?((\\\\mathrm{replicate}(n,l)).flatten) = List.getLast?(l).$$$$

Lean4

@[simp]
theorem getLast?_flatten_replicate {n : ℕ} (h : n ≠ 0) (l : List α) :
    (List.replicate n l).flatten.getLast? = l.getLast? := by
  rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate, List.reverse_replicate,
    head?_flatten_replicate h]

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