Documentation

Mathlib.Tactic.Continuity

Continuity #

We define the continuity tactic using aesop.

source
def attrContinuity :
Lean.ParserDescr

The continuity attribute used to tag continuity statements for the continuity tactic.

Equations
    Instances For
      source
      def tacticContinuity :
      Lean.ParserDescr

      The tactic continuity solves goals of the form Continuous f by applying lemmas tagged with the continuity user attribute.

      fun_prop is a (usually more powerful) alternative to continuity.

      Equations
        Instances For
          source
          def tacticContinuity? :
          Lean.ParserDescr

          The tactic continuity solves goals of the form Continuous f by applying lemmas tagged with the continuity user attribute.

          Equations
            Instances For