mathlib3 documentation

core / init.data.subtype.basic

theorem subtype.exists_of_subtype {α : Type u} {p : α Prop} :
{x // p x} ( (x : α), p x)
theorem subtype.tag_irrelevant {α : Type u} {p : α Prop} {a : α} (h1 h2 : p a) :
a, h1⟩ = a, h2⟩
@[protected]
theorem subtype.eq {α : Type u} {p : α Prop} {a1 a2 : {x // p x}} :
a1.val = a2.val a1 = a2
theorem subtype.ne_of_val_ne {α : Type u} {p : α Prop} {a1 a2 : {x // p x}} :
a1.val a2.val a1 a2
theorem subtype.eta {α : Type u} {p : α Prop} (a : {x // p x}) (h : p a.val) :
a.val, h⟩ = a
def subtype.inhabited {α : Type u} {p : α Prop} {a : α} (h : p a) :
inhabited {x // p x}
Equations