Theorems · Inductive type · general algebraic systems

IsNegApply

(F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Neg β] → [Neg F] → Prop

IsNegApply F α β states for all f : F and x : α, (-f) x = -f x.

Defined in

Mathlib.Data.FunLike.IsApply

Cited by

21 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

FunLikeNegNeg