Documentation

Mathlib.Tactic.Monotonicity.Attr

The @[mono] attribute #

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

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