instDecidablePredMemSetFixedByOfDecidableEq

English

If β has a decidable equality, then for every m ∈ M, the predicate b ↦ (b ∈ fixedBy β m) is decidable.

Русский

Если на β задано разрешимое равенство, то для каждого m ∈ M предикат b ⇢ b фиксировано рабос фиксацией (fixedBy β m) разрешим.

LaTeX

$$ (m : M) [DecidableEq β] : DecidablePred (\lambda b : β, b ∈ fixedBy β m)$$

Lean4

@[to_additive instDecidablePredMemSetFixedByAddOfDecidableEq]
instance (m : M) [DecidableEq β] : DecidablePred fun b : β => b ∈ MulAction.fixedBy β m := fun b ↦
  by
  simp only [MulAction.mem_fixedBy]
  infer_instance

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