zipRight_eq_zipRight'

Mathlib.Data.List.Map2

URI: https://scilib.ai/kg/mathlib#List.zipRight_eq_zipRight'

English

For lists as, bs, zipRight as bs equals the first projection of zipRight'(as, bs).

Русский

Для списков as, bs zipRight as bs равно первой компоненте zipRight'(as, bs).

LaTeX

$$$ \operatorname{zipRight}(as, bs) = \operatorname{fst}(\operatorname{zipRight}'(as, bs))$$$

Lean4

theorem zipRight_eq_zipRight' : zipRight as bs = (zipRight' as bs).fst := by
  induction as generalizing bs <;> cases bs <;> simp [*]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru