map_id — Mathlib

English

Mapping the identity function over a sequence yields the sequence itself.

Русский

Преобразование идентичной функцией над последовательностью возвращает саму последовательность.

LaTeX

$$$\forall s : Seq \alpha, map id s = s$$$

Lean4

@[simp]
theorem map_id : ∀ s : Seq α, map id s = s
  | ⟨s, al⟩ => by
    apply Subtype.eq; dsimp [map]
    rw [Option.map_id, Stream'.map_id]

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