map_get? — Mathlib

English

For any function f, and any a, the nth element gotten from map f s equals the mapped nth element of s.

Русский

Для любой функции f и элемента a первый элемент из map f s равен отображению первого элемента s через f.

LaTeX

$$$\forall {f : \alpha \to \beta} {s : Seq \alpha} {n},\; get? (map f s) n = (get? s n).map f$$$

Lean4

@[simp]
theorem map_get? (f : α → β) : ∀ s n, get? (map f s) n = (get? s n).map f
  | ⟨_, _⟩, _ => rfl

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