English
For g : γ → α and a symmetric f, lifting after mapping satisfies lift f (map g p) = lift ⟨c1,c2 ↦ f(g c1, g c2), …⟩ p.
Русский
Для отображения g: γ→α и симметричной f имеет место равенство: lift f (map g p) = lift ⟨c1,c2 ↦ f(g c1, g c2), …⟩ p.
LaTeX
$$$ \\mathrm{lift} f\\ (\\mathrm{map} \\, g \\ p) = \\mathrm{lift} \\langle \\lambda (c_1,c_2):\\gamma\\times\\gamma, f\\.val\\ (g\\,c_1)\\ (g\\,c_2), \\dots \\rangle \\ p. $$$
Lean4
theorem lift_map_apply {g : γ → α} (f : { f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁ }) (p : Sym2 γ) :
lift f (map g p) = lift ⟨fun (c₁ c₂ : γ) => f.val (g c₁) (g c₂), fun _ _ => f.prop _ _⟩ p := by
conv_rhs => rw [← lift_comp_map, comp_apply]
