instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq

English

If α has decidable equality, then for every a ∈ α, the predicate m ↦ m ∈ stabilizerSubmonoid M a is decidable.

Русский

Если для α дано разрешимое сравнение, то для каждого a ∈ α предикат принадлежности m ∈ stabilizerSubmonoid M a разрешим.

LaTeX

$$$$ [DecidableEq \\alpha] \\Rightarrow \\forall a : \\alpha, \\ Decidable (\\, m \\in stabilizerSubmonoid M a \,). $$$$

Lean4

@[to_additive]
instance [DecidableEq α] (a : α) : DecidablePred (· ∈ stabilizerSubmonoid M a) := fun _ =>
  inferInstanceAs <| Decidable (_ = _)

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