decidableMemProd — Mathlib

English

There is a decidable predicate for membership in the product s × t provided decidable predicates for membership in s and t hold.

Русский

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

LaTeX

$$[DecidablePred (x ∈ s)] → [DecidablePred (x ∈ t)] → DecidablePred (x ∈ s × t)$$

Lean4

instance decidableMemProd [DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)] : DecidablePred (· ∈ s ×ˢ t) := fun x =>
  inferInstanceAs (Decidable (x.1 ∈ s ∧ x.2 ∈ t))

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