# Tactics for the continuous functional calculus #

At the moment, these tactics are just wrappers, but potentially they could be more sophisticated.

source
def cfcTac :
Lean.ParserDescr

A tactic used to automatically discharge goals relating to the continuous functional calculus, specifically whether the element satisfies the predicate.

Equations

- cfcTac = Lean.ParserDescr.node `cfcTac 1024 (Lean.ParserDescr.nonReservedSymbol "cfc_tac" false)

Instances For

source
def cfcContTac :
Lean.ParserDescr

A tactic used to automatically discharge goals relating to the continuous functional calculus, specifically concerning continuity of the functions involved.

Equations

- cfcContTac = Lean.ParserDescr.node `cfcContTac 1024 (Lean.ParserDescr.nonReservedSymbol "cfc_cont_tac" false)

Instances For

source
def cfcZeroTac :
Lean.ParserDescr

A tactic used to automatically discharge goals relating to the non-unital continuous functional calculus, specifically concerning whether `f 0 = 0`.

Equations

- cfcZeroTac = Lean.ParserDescr.node `cfcZeroTac 1024 (Lean.ParserDescr.nonReservedSymbol "cfc_zero_tac" false)

Instances For