mathlib documentation

data.subtype

Subtypes #

This file provides basic API for subtypes, which are defined in core.

A subtype is a type made from restricting another type, say α, to its elements that satisfy some predicate, say p : α → Prop. Specifically, it is the type of pairs ⟨val, property⟩ where val : α and property : p val. It is denoted subtype p and notation {val : α // p val} is available.

A subtype has a natural coercion to the parent type, by coercing ⟨val, property⟩ to val. As such, subtypes can be thought of as bundled sets, the difference being that elements of a set are still of type α while elements of a subtype aren't.

def subtype.simps.coe {α : Sort u_1} {p : α → Prop} (x : subtype p) :
α

See Note [custom simps projection]

Equations
theorem subtype.prop {α : Sort u_1} {p : α → Prop} (x : subtype p) :
p x

A version of x.property or x.2 where p is syntactically applied to the coercion of x instead of x.1. A similar result is subtype.mem in data.set.basic.

@[simp]
theorem subtype.val_eq_coe {α : Sort u_1} {p : α → Prop} {x : subtype p} :
x.val = x
@[protected, simp]
theorem subtype.forall {α : Sort u_1} {p : α → Prop} {q : {a // p a} → Prop} :
(∀ (x : {a // p a}), q x) ∀ (a : α) (b : p a), q a, b⟩
@[protected]
theorem subtype.forall' {α : Sort u_1} {p : α → Prop} {q : Π (x : α), p x → Prop} :
(∀ (x : α) (h : p x), q x h) ∀ (x : {a // p a}), q x _

An alternative version of subtype.forall. This one is useful if Lean cannot figure out q when using subtype.forall from right to left.

@[protected, simp]
theorem subtype.exists {α : Sort u_1} {p : α → Prop} {q : {a // p a} → Prop} :
(∃ (x : {a // p a}), q x) ∃ (a : α) (b : p a), q a, b⟩
@[protected]
theorem subtype.exists' {α : Sort u_1} {p : α → Prop} {q : Π (x : α), p x → Prop} :
(∃ (x : α) (h : p x), q x h) ∃ (x : {a // p a}), q x _

An alternative version of subtype.exists. This one is useful if Lean cannot figure out q when using subtype.exists from right to left.

@[protected, ext]
theorem subtype.ext {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :
a1 = a2a1 = a2
theorem subtype.ext_iff {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :
a1 = a2 a1 = a2
theorem subtype.heq_iff_coe_eq {α : Sort u_1} {p q : α → Prop} (h : ∀ (x : α), p x q x) {a1 : {x // p x}} {a2 : {x // q x}} :
a1 == a2 a1 = a2
theorem subtype.heq_iff_coe_heq {α β : Sort u_1} {p : α → Prop} {q : β → Prop} {a : {x // p x}} {b : {y // q y}} (h : α = β) (h' : p == q) :
a == b a == b
theorem subtype.ext_val {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :
a1.val = a2.vala1 = a2
theorem subtype.ext_iff_val {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :
a1 = a2 a1.val = a2.val
@[simp]
theorem subtype.coe_eta {α : Sort u_1} {p : α → Prop} (a : {a // p a}) (h : p a) :
a, h⟩ = a
@[simp]
theorem subtype.coe_mk {α : Sort u_1} {p : α → Prop} (a : α) (h : p a) :
a, h⟩ = a
@[simp, nolint]
theorem subtype.mk_eq_mk {α : Sort u_1} {p : α → Prop} {a : α} {h : p a} {a' : α} {h' : p a'} :
a, h⟩ = a', h'⟩ a = a'
theorem subtype.coe_eq_of_eq_mk {α : Sort u_1} {p : α → Prop} {a : {a // p a}} {b : α} (h : a = b) :
a = b, _⟩
theorem subtype.coe_eq_iff {α : Sort u_1} {p : α → Prop} {a : {a // p a}} {b : α} :
a = b ∃ (h : p b), a = b, h⟩
theorem subtype.coe_injective {α : Sort u_1} {p : α → Prop} :
theorem subtype.val_injective {α : Sort u_1} {p : α → Prop} :
theorem subtype.coe_inj {α : Sort u_1} {p : α → Prop} {a b : subtype p} :
a = b a = b
theorem subtype.val_inj {α : Sort u_1} {p : α → Prop} {a b : subtype p} :
a.val = b.val a = b
@[simp]
theorem exists_eq_subtype_mk_iff {α : Sort u_1} {p : α → Prop} {a : subtype p} {b : α} :
(∃ (h : p b), a = b, h⟩) a = b
@[simp]
theorem exists_subtype_mk_eq_iff {α : Sort u_1} {p : α → Prop} {a : subtype p} {b : α} :
(∃ (h : p b), b, h⟩ = a) b = a
def subtype.restrict {α : Sort u_1} {β : α → Type u_2} (p : α → Prop) (f : Π (x : α), β x) (x : subtype p) :
β x.val

Restrict a (dependent) function to a subtype

Equations
theorem subtype.restrict_apply {α : Sort u_1} {β : α → Type u_2} (f : Π (x : α), β x) (p : α → Prop) (x : subtype p) :
theorem subtype.restrict_def {α : Sort u_1} {β : Type u_2} (f : α → β) (p : α → Prop) :
theorem subtype.restrict_injective {α : Sort u_1} {β : Type u_2} {f : α → β} (p : α → Prop) (h : function.injective f) :
theorem subtype.surjective_restrict {α : Sort u_1} {β : α → Type u_2} [ne : ∀ (a : α), nonempty (β a)] (p : α → Prop) :
function.surjective (λ (f : Π (x : α), β x), subtype.restrict p f)
@[simp]
theorem subtype.coind_coe {α : Sort u_1} {β : Sort u_2} (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)) (ᾰ : α) :
(subtype.coind f h ᾰ) = f ᾰ
def subtype.coind {α : Sort u_1} {β : Sort u_2} (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)) :
α → subtype p

Defining a map into a subtype, this can be seen as an "coinduction principle" of subtype

Equations
theorem subtype.coind_injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : function.injective f) :
theorem subtype.coind_surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : function.surjective f) :
theorem subtype.coind_bijective {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : function.bijective f) :
@[simp]
theorem subtype.map_coe {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p aq (f a)) (ᾰ : subtype p) :
(subtype.map f h ᾰ) = f
def subtype.map {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p aq (f a)) :

Restriction of a function to a function on subtypes.

Equations
theorem subtype.map_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p : α → Prop} {q : β → Prop} {r : γ → Prop} {x : subtype p} (f : α → β) (h : ∀ (a : α), p aq (f a)) (g : β → γ) (l : ∀ (a : β), q ar (g a)) :
subtype.map g l (subtype.map f h x) = subtype.map (g f) _ x
theorem subtype.map_id {α : Sort u_1} {p : α → Prop} {h : ∀ (a : α), p ap (id a)} :
theorem subtype.map_injective {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ (a : α), p aq (f a)) (hf : function.injective f) :
theorem subtype.map_involutive {α : Sort u_1} {p : α → Prop} {f : α → α} (h : ∀ (a : α), p ap (f a)) (hf : function.involutive f) :
@[protected, instance]
def subtype.has_equiv {α : Sort u_1} [has_equiv α] (p : α → Prop) :
Equations
theorem subtype.equiv_iff {α : Sort u_1} [has_equiv α] {p : α → Prop} {s t : subtype p} :
s t s t
@[protected]
theorem subtype.refl {α : Sort u_1} {p : α → Prop} [setoid α] (s : subtype p) :
s s
@[protected]
theorem subtype.symm {α : Sort u_1} {p : α → Prop} [setoid α] {s t : subtype p} (h : s t) :
t s
@[protected]
theorem subtype.trans {α : Sort u_1} {p : α → Prop} [setoid α] {s t u : subtype p} (h₁ : s t) (h₂ : t u) :
s u
theorem subtype.equivalence {α : Sort u_1} [setoid α] (p : α → Prop) :
@[protected, instance]
def subtype.setoid {α : Sort u_1} [setoid α] (p : α → Prop) :
Equations

Some facts about sets, which require that α is a type.

@[simp]
theorem subtype.coe_prop {α : Type u_1} {S : set α} (a : {a // a S}) :
a S
theorem subtype.val_prop {α : Type u_1} {S : set α} (a : {a // a S}) :
a.val S