addBottom_map — Mathlib

English

Mapping the snd projection after addBottom recovers the original list: (addBottom L).map snd = L.

Русский

Отображение snd после addBottom восстанавливает исходный список: (addBottom L).map snd = L.

LaTeX

$$$ (\mathrm{addBottom} \, L).map \langle \mathrm{snd}, \cdot \rangle = L $$$

Lean4

theorem addBottom_map (L : ListBlank (∀ k, Option (Γ k))) : (addBottom L).map ⟨Prod.snd, by rfl⟩ = L :=
  by
  simp only [addBottom, ListBlank.map_cons]
  convert ListBlank.cons_head_tail L
  generalize ListBlank.tail L = L'
  refine L'.induction_on fun l ↦ ?_; simp

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