English
The process of mapping by a function commutes with the permutation relation in a precise way: the relation defined by equality after mapping composed with permutation equals the permutation-after-mapping relation.
Русский
Процесс отображения по функции совместим с отношением перестановки: отношение, задаваемое равенством после отображения, композиция с перестановкой равна отношению перестановки после отображения.
LaTeX
$$$(\\cdot = \\mathrm{map}(f, \\cdot)) \\circ_r (\\cdot \\sim \\cdot) = (\\cdot \\sim \\mathrm{map}(f, \\cdot))$$$
Lean4
theorem eq_map_comp_perm (f : α → β) : (· = map f ·) ∘r (· ~ ·) = (· ~ map f ·) :=
by
conv_rhs => rw [← Relation.comp_eq_fun (map f)]
simp only [← forall₂_eq_eq_eq, forall₂_map_right_iff, forall₂_comp_perm_eq_perm_comp_forall₂]
