instDecidablePredMemSubgroupStabilizerOfDecidableEq

English

If α has decidable equality, then membership to the stabilizer is decidable as a predicate on α.

Русский

Если равенство в α разрешимо, то принадлежность элементу стабилизатора распознаётся какDecidablePred.

LaTeX

$$instance [DecidableEq α] (a : α) : DecidablePred (fun g => g ∈ MulAction.stabilizer G a)$$

Lean4

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

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