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