instDecidableRelSSubset — Mathlib

English

If α has decidable equality, then the strict subset relation on Finset α is decidable.

Русский

Если у α задано разрешимое равенство, то отношение строгого включения между конечными подмножствами Finset α разрешимо.

LaTeX

$$$\\forall s,t:\\ Finset\\ \\alpha,\\ Decidable\\ (s\\subsetneq t)$$$

Lean4

instance instDecidableRelSSubset [DecidableEq α] : DecidableRel (α := Finset α) (· ⊂ ·) := fun _ _ ↦ instDecidableAnd

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