English
There is a natural equivalence between AddConstMap G H a b and itself given by f ↦ (x ↦ −f(−x)). This is an involutive symmetry of affine maps.
Русский
Существует естественное взаимнооднозначное соответствие между AddConstMap G H a b и самим собой, заданное отображением f ↦ (x ↦ −f(−x)); это инволютивное симметрическое преобразование.
LaTeX
$$$\text{conjNeg}: (G \to+c[a,b] H) \simeq (G \to+c[a,b] H),\; f \mapsto (x \mapsto -f(-x)).$$$
Lean4
/-- If `f : G → H` is an `AddConstMap`, then so is `fun x ↦ -f (-x)`. -/
@[simps! apply_coe]
def conjNeg : (G →+c[a, b] H) ≃ (G →+c[a, b] H) :=
Involutive.toPerm (fun f ↦ ⟨fun x ↦ -f (-x), fun _ ↦ by simp [neg_add_eq_sub]⟩) fun _ ↦
AddConstMap.ext fun _ ↦ by simp
