mathlib documentation

core.init.data.subtype.instances

@[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 (λ (a : val = w_val), eq.rec (λ (w_property : p val), is_true _) a w_property) (λ (a : ¬val = w_val), is_false _))))