evalFinsetDens

Mathlib.Tactic.Positivity.Finset

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

Lean4

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

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

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

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

Разделы

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

Аффилиация

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