Finiteness tactic #
This file implements a basic finiteness
tactic, designed to solve goals of the form *** < ∞
and
(equivalently) *** ≠ ∞
in the extended nonnegative reals (ENNReal
, aka ℝ≥0∞
).
It works recursively according to the syntax of the expression. It is implemented as an aesop
rule
set.
TODO: improve finiteness
to also deal with other situations, such as balls in proper spaces with
a locally finite measure.
Lemmas #
Tactic implementation #
A version of the positivity tactic for use by aesop
.
Equations
- PositivityForAesop = Lean.Elab.Tactic.liftMetaTactic fun (g : Lean.MVarId) => do Mathlib.Meta.Positivity.positivity g pure []
Instances For
Tactic to solve goals of the form *** < ∞
and (equivalently) *** ≠ ∞
in the extended
nonnegative reals (ℝ≥0∞
).
Equations
- One or more equations did not get rendered due to their size.