Documentation

Mathlib.Tactic.Monotonicity.Attr

The @[mono] attribute #

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