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

Adding @[to_fun] to a lemma

theorem Continuous.mul (hf : Continuous f) (hg : Continuous g) : Continuous (f * g)

will generate a new lemma Continuous.fun_mul with conclusion Continuous 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.