Documentation

Mathlib.Tactic.Positivity.Finset

Positivity extensions for finsets #

This file provides a few positivity extensions that cannot be in either the finset files (because they don't know about ordered fields) or in Tactic.Positivity.Basic (because it doesn't want to know about finiteness).

Extension for Finset.card. s.card is positive if s is nonempty.

It calls Mathlib.Meta.proveFinsetNonempty to attempt proving that the finset is nonempty.

Instances For

    Extension for Finset.dens. s.card is positive if s is nonempty.

    It calls Mathlib.Meta.proveFinsetNonempty to attempt proving that the finset is nonempty.

    Instances For