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).

source
def Mathlib.Meta.Positivity.evalFinsetCard :
Mathlib.Meta.Positivity.PositivityExt

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
    source
    def Mathlib.Meta.Positivity.evalFintypeCard :
    Mathlib.Meta.Positivity.PositivityExt

    Extension for Fintype.card. Fintype.card α is positive if α is nonempty.

    Instances For
      source
      def Mathlib.Meta.Positivity.evalFinsetDens :
      Mathlib.Meta.Positivity.PositivityExt

      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