Set-subset decidability over finite types

Set.decidableSubsetOfFintype derives Decidable (s ⊆ t) from Fintype plus decidable membership. Deliberately a def, not an instance, following mathlib's Set.decidableMemOfFintype: global Decidable instances on Set relations risk instance loops and higher-order DecidablePred searches. Activate with attribute [local instance] Set.decidableSubsetOfFintype.

@[implicit_reducible]

def Set.decidableSubsetOfFintype {α : Type u_1} [Fintype α] (s t : Set α) [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : α) => x ∈ t] : Decidable (s ⊆ t)

Decidable (s ⊆ t) from Fintype plus decidable membership. Not an instance; activate locally.

Equations

• s.decidableSubsetOfFintype t = inferInstance