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
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
    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
        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
            Instances For