Documentation

Mathlib.Tactic.ContinuousFunctionalCalculus

Tactics for the continuous functional calculus #

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

source
🔸 coverage
def cfcTac :
Lean.ParserDescr

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

Instances For
    source
    🔸 coverage
    def cfcContTac :
    Lean.ParserDescr

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

    Instances For
      source
      🔸 coverage
      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.

      Instances For