decidableMemPowers — Mathlib

English

Membership in powers(a) is decidable (under classical logic).

Русский

Членство в powers(a) разрешимо (при классической логике).

LaTeX

$$$\\\\operatorname{DecidablePred}(\\\\lambda x, x \\\\in \\\\mathrm{powers}(a))$$$

Lean4

noncomputable instance decidableMemPowers : DecidablePred (· ∈ Submonoid.powers a) :=
  Classical.decPred
    _
      -- TODO the following instance should follow from a more general principle
      -- See also https://github.com/leanprover-community/mathlib4/issues/2417

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