instDecidablePredMemSetSupportOfLeAtTop

English

There is a decidability instance for membership in the support of L when L ≤ atTop.

Русский

Существует конструкция разрешимости принадлежности к поддержке L при L ≤ atTop.

LaTeX

$$$ \text{instance } (L : SummationFilter \beta) [L.LeAtTop] : DecidablePred (\cdot \in L.support) $$$

Lean4

/-- Decidability instance: useful when working with `Finset` sums / products. -/
instance (L : SummationFilter β) [L.LeAtTop] : DecidablePred (· ∈ L.support) := fun b ↦ isTrue (by simp)

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