Bounds Module Index

This module re-exports all components of the bounds verification infrastructure.

Submodules

• Core: Basic boolean checkers and golden theorems for bound verification
• Checked: Support for expressions with inverse-like operations (inv, log, atan, etc.)
• Smart: Monotonicity-aware bounds using derivative information
• Bridge: Set.Icc bridge theorems and subdivision combinators

Usage

Import this module to get access to all bound verification functionality:

import LeanCert.Validity.Bounds.Basic