core / init.data.subtype.basic - mathlib3 docs

mathlib3 documentation

core / init.data.subtype.basic

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