mathlib documentation

core.init.data.subtype.basic

def 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⟩

theorem subtype.eq {α : Type u} {p : α → Prop} {a1 a2 : {x // p x}} :
a1.val = a2.vala1 = a2

theorem subtype.ne_of_val_ne {α : Type u} {p : α → Prop} {a1 a2 : {x // p x}} :
a1.val a2.vala1 a2

@[simp]
theorem subtype.eta {α : Type u} {p : α → Prop} (a : {x // p x}) (h : p a.val) :
a.val, h⟩ = a

@[instance]
def subtype.inhabited {α : Type u} {p : α → Prop} {a : α} :
p ainhabited {x // p x}

Equations