evalFinsetCard

Mathlib.Tactic.Positivity.Finset

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.Positivity.evalFinsetCard

Lean4

/-- Extension for `Finset.card`. `#s` is positive if `s` is nonempty.

It calls `Mathlib.Meta.proveFinsetNonempty` to attempt proving that the finset is nonempty. -/
@[positivity Finset.card _]
def evalFinsetCard : PositivityExt where
  eval {u α} _ _
    e := do
    match u, α, e with
    | 0, ~q(ℕ), ~q(Finset.card $s) =>
      let some ps ← proveFinsetNonempty s |
        return .none
      assertInstancesCommute
      return .positive q(Finset.Nonempty.card_pos $ps)
    | _ =>
      throwError"not Finset.card"

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru