Documentation

Mathlib.Tactic.Monotonicity.Attr

The @[mono] attribute #

source
def Mathlib.Tactic.Monotonicity.mono.side :
Lean.ParserDescr
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.

    Instances For
      source
      opaque Mathlib.Tactic.Monotonicity.Attr.ext :
      Std.Tactic.LabelAttr.LabelExtension

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