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