evalTriangleRemovalBound — Mathlib

Lean4

/-- Extension for the `positivity` tactic: `SimpleGraph.triangleRemovalBound ε` is positive
if `ε` is.

This exploits the positivity of the junk value of `triangleRemovalBound ε` for `ε ≥ 1`. -/
@[positivity triangleRemovalBound _]
def evalTriangleRemovalBound : PositivityExt where
  eval {u α} _zα _pα
    e := do
    match u, α, e with
    | 0, ~q(ℝ), ~q(triangleRemovalBound $ε) =>
      let .positive hε ← core q(inferInstance) q(inferInstance) ε |
        failure
      assertInstancesCommute
      pure (.positive q(triangleRemovalBound_pos $hε))
    | _, _, _ =>
      throwError"failed to match on Int.ceil application"

Похожие утверждения