map_congr — Mathlib

English

If s1 ~ s2, then map f s1 ~ map f s2.

Русский

Если s1 эквивалентно s2, то map f s1 эквивалентно map f s2.

LaTeX

$$$\\forall {s1 s2 : Computation\\alpha}\\ {f:\\alpha\\to\\beta},\\ s1 \\sim s2 \\Rightarrow (\\mathrm{map}\\ f\\ s1) \\sim (\\mathrm{map}\\ f\\ s2)$$$

Lean4

theorem map_congr {s1 s2 : Computation α} {f : α → β} (h1 : s1 ~ s2) : map f s1 ~ map f s2 :=
  by
  rw [← lift_eq_iff_equiv]
  exact liftRel_map Eq _ ((lift_eq_iff_equiv _ _).2 h1) fun {a} b => congr_arg _

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