decidableMemMul — Mathlib

English

There is a decidable predicate for membership in s * t, assuming decidable membership in s and t (and finiteness of the ambient type).

Русский

Существует разрешимое предикат для принадлежности в s * t, если заданыDecidablePred (принадлежность в s) и DecidablePred (принадлежность в t) (и конечность типа).

LaTeX

$$$$ [Fintype \\; \\alpha] [DecidableEq \\; \\alpha] [DecidablePred (\\cdot \\in s)] [DecidablePred (\\cdot \\in t)] \\Rightarrow DecidablePred (\\cdot \\in s * t) $$$$

Lean4

@[to_additive]
instance decidableMemMul [Fintype α] [DecidableEq α] [DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)] :
    DecidablePred (· ∈ s * t) := fun _ ↦ decidable_of_iff _ mem_mul.symm

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