decidableMemPow — Mathlib

English

There is a decidable predicate for membership in s^n for all n, given a finite ambient type and decidable membership in s.

Русский

Существует разрешимый предикат принадлежности в s^n для всех n, при условии конечности типа и decidable_MEMBERSHIP(s).

LaTeX

$$$$ [Fintype \\; \\alpha] [DecidableEq \\; \\alpha] [DecidablePred (\\cdot \\in s)] (n : \\mathbb{N}) \\Rightarrow DecidablePred (\\cdot \\in s^n) $$$$

Lean4

@[to_additive]
instance decidableMemPow [Fintype α] [DecidableEq α] [DecidablePred (· ∈ s)] (n : ℕ) : DecidablePred (· ∈ s ^ n) := by
  induction n with
  | zero =>
    simp only [pow_zero, mem_one]
    infer_instance
  | succ n ih =>
    rw [pow_succ]
    infer_instance

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