Tactics for the continuous functional calculus #
At the moment, these tactics are just wrappers, but potentially they could be more sophisticated.
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
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
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)