HepLean Documentation

Mathlib.Tactic.Monotonicity.Attr

The @[mono] attribute #

source
def Mathlib.Tactic.Monotonicity.mono.side :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
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
    • One or more equations did not get rendered due to their size.
    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.