map₂Right_eq_map₂Right' — Mathlib

English

For any f, as, bs, map₂Right f as bs equals the fst component of map₂Right' f as bs.

Русский

Для любого f, as, bs, map₂Right f as bs равен fst части пары (map₂Right' f as bs).

LaTeX

$$$\\forall f:\\alpha \\to \\mathrm{Option}\\,\\beta \\to \\gamma\\ ,\\ \\forall as bs,\\ \\mathrm{map₂Right}\\ f\\ as\\ bs = (\\mathrm{map₂Right}'\\ f\\ as\\ bs).fst$$$

Lean4

theorem map₂Right_eq_map₂Right' : map₂Right f as bs = (map₂Right' f as bs).fst := by
  simp only [map₂Right, map₂Right', map₂Left_eq_map₂Left']

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