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.

You can specify the name of the new declaration manually, as in @[to_fun Differentiable.fun_mul]. If you do so, the newly generated name is namespaced to match the original declaration's name: tagging Foo.bar with to_fun baz generates Foo.baz; tagging Foo.Bar.baz with Bars.baz generates Foo.Bars.baz, etc.

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

Equations

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