Documentation

Mathlib.Tactic.Monotonicity.Attr

The @[mono] attribute #

source
def Mathlib.Tactic.Monotonicity.mono.side :
Lean.ParserDescr
Equations
    Instances For
      source
      def Mathlib.Tactic.Monotonicity.Attr.mono :
      Lean.ParserDescr

      A lemma stating the monotonicity of some function, with respect to appropriate relations on its domain and range, and possibly with side conditions.

      Equations
        Instances For
          source
          opaque Mathlib.Tactic.Monotonicity.Attr.ext :
          Lean.LabelExtension

          A lemma stating the monotonicity of some function, with respect to appropriate relations on its domain and range, and possibly with side conditions.