The to_fun attribute

Adding @[to_fun] to a lemma named foo creates a new lemma named fun_foo, which is obtained by running pull fun _ ↦ _ on the type of F. This can be useful for generating the applied form of a continuity lemma from the unapplied form.

def Mathlib.Tactic.to_fun : Lean.ParserDescr

Generate an eta-expanded version of a lemma. Adding @[to_fun] to a lemma written in "point-free" form, e.g.

theorem Differentiable.mul (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) :
    Differentiable 𝕜 (f * g)

will generate a new lemma Differentiable.fun_mul with conclusion Differentiable 𝕜 fun x => f x * g x.

Use the to_fun (attr := ...) syntax to add the same attribute to both declarations.

Equations

• One or more equations did not get rendered due to their size.