map_congr — Mathlib

English

If two WSeq α sequences s and t are equivalent (s ~ʷ t), then applying a fixed function f : α → β to both yields two equivalent WSeq β sequences (map f s ~ʷ map f t).

Русский

Если две последовательности-потока WSeq α, s и t, эквивалентны (s ~ʷ t), то применение фиксированной функции f : α → β к обеим сохраняет эквивалентность: map f s ~ʷ map f t.

LaTeX

$$$ \forall f : \alpha \to \beta,\; \forall s,t : \mathrm{WSeq}\,\alpha,\; s \sim_W t \Rightarrow \mathrm{map}\,f\,s \sim_W \mathrm{map}\,f\,t $$$

Lean4

theorem map_congr (f : α → β) {s t : WSeq α} (h : s ~ʷ t) : map f s ~ʷ map f t :=
  liftRel_map _ _ h fun {_ _} => congr_arg _

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