mathlib documentation

core / init.data.subtype.instances

source
@[protected, instance]
def subtype.decidable_eq {α : Type u} {p : α → Prop} [decidable_eq α] :
decidable_eq {x // p x}
Equations
  • subtype.decidable_eq = id (λ (_v : {x // p x}), _v.cases_on (λ (val : α) (property : p val) (w : {x // p x}), w.cases_on (λ (w_val : α) (w_property : p w_val), decidable.by_cases (λ (ᾰ : val = w_val), eq.rec (λ (w_property : p val), is_true _) ᾰ w_property) (λ (ᾰ : ¬val = w_val), is_false _))))