# Documentation

Mathlib.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.

theorem Subtype.prop {α : Sort u_1} {p : αProp} (x : ) :
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.forall {α : Sort u_1} {p : αProp} {q : { a // p a }Prop} :
((x : { a // p a }) → q x) (a : α) → (b : p a) → q { val := a, property := b }
theorem Subtype.forall' {α : Sort u_1} {p : αProp} {q : (x : α) → p xProp} :
((x : α) → (h : p x) → q x h) (x : { a // p a }) → q (x) x.property

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

@[simp]
theorem Subtype.exists {α : Sort u_1} {p : αProp} {q : { a // p a }Prop} :
(x, q x) a b, q { val := a, property := b }
theorem Subtype.exists' {α : Sort u_1} {p : αProp} {q : (x : α) → p xProp} :
(x h, q x h) x, q (x) x.property

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

theorem Subtype.ext {α : Sort u_1} {p : αProp} {a1 : { x // p x }} {a2 : { x // p x }} :
a1 = a2a1 = a2
theorem Subtype.ext_iff {α : Sort u_1} {p : αProp} {a1 : { x // p x }} {a2 : { x // p x }} :
a1 = a2 a1 = a2
theorem Subtype.heq_iff_coe_eq {α : Sort u_1} {p : αProp} {q : αProp} (h : ∀ (x : α), p x q x) {a1 : { x // p x }} {a2 : { x // q x }} :
HEq a1 a2 a1 = a2
theorem Subtype.heq_iff_coe_heq {α : Sort u_4} {β : Sort u_4} {p : αProp} {q : βProp} {a : { x // p x }} {b : { y // q y }} (h : α = β) (h' : HEq p q) :
HEq a b HEq a b
theorem Subtype.ext_val {α : Sort u_1} {p : αProp} {a1 : { x // p x }} {a2 : { x // p x }} :
a1 = a2a1 = a2
theorem Subtype.ext_iff_val {α : Sort u_1} {p : αProp} {a1 : { x // p x }} {a2 : { x // p x }} :
a1 = a2 a1 = a2
@[simp]
theorem Subtype.coe_eta {α : Sort u_1} {p : αProp} (a : { a // p a }) (h : p a) :
{ val := a, property := h } = a
theorem Subtype.coe_mk {α : Sort u_1} {p : αProp} (a : α) (h : p a) :
{ val := a, property := h } = a
theorem Subtype.mk_eq_mk {α : Sort u_1} {p : αProp} {a : α} {h : p a} {a' : α} {h' : p a'} :
{ val := a, property := h } = { val := a', property := h' } a = a'
theorem Subtype.coe_eq_of_eq_mk {α : Sort u_1} {p : αProp} {a : { a // p a }} {b : α} (h : a = b) :
a = { val := b, property := ha.property }
theorem Subtype.coe_eq_iff {α : Sort u_1} {p : αProp} {a : { a // p a }} {b : α} :
a = b h, a = { val := b, property := h }
theorem Subtype.coe_injective {α : Sort u_1} {p : αProp} :
Function.Injective fun a => a
theorem Subtype.val_injective {α : Sort u_1} {p : αProp} :
Function.Injective Subtype.val
theorem Subtype.coe_inj {α : Sort u_1} {p : αProp} {a : } {b : } :
a = b a = b
theorem Subtype.val_inj {α : Sort u_1} {p : αProp} {a : } {b : } :
a = b a = b
@[simp]
theorem exists_eq_subtype_mk_iff {α : Sort u_1} {p : αProp} {a : } {b : α} :
(h, a = { val := b, property := h }) a = b
@[simp]
theorem exists_subtype_mk_eq_iff {α : Sort u_1} {p : αProp} {a : } {b : α} :
(h, { val := b, property := h } = a) b = a
def Subtype.restrict {α : Sort u_5} {β : αType u_4} (p : αProp) (f : (x : α) → β x) (x : ) :
β x

Restrict a (dependent) function to a subtype

Instances For
theorem Subtype.restrict_apply {α : Sort u_5} {β : αType u_4} (f : (x : α) → β x) (p : αProp) (x : ) :
= f x
theorem Subtype.restrict_def {α : Sort u_4} {β : Type u_5} (f : αβ) (p : αProp) :
= f fun a => a
theorem Subtype.restrict_injective {α : Sort u_4} {β : Type u_5} {f : αβ} (p : αProp) (h : ) :
theorem Subtype.surjective_restrict {α : Sort u_5} {β : αType u_4} [ne : ∀ (a : α), Nonempty (β a)] (p : αProp) :
@[simp]
theorem Subtype.coind_coe {α : Sort u_4} {β : Sort u_5} (f : αβ) {p : βProp} (h : (a : α) → p (f a)) :
∀ (a : α), ↑() = f a
def Subtype.coind {α : Sort u_4} {β : Sort u_5} (f : αβ) {p : βProp} (h : (a : α) → p (f a)) :
α

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

Instances For
theorem Subtype.coind_injective {α : Sort u_4} {β : Sort u_5} {f : αβ} {p : βProp} (h : (a : α) → p (f a)) (hf : ) :
theorem Subtype.coind_surjective {α : Sort u_4} {β : Sort u_5} {f : αβ} {p : βProp} (h : (a : α) → p (f a)) (hf : ) :
theorem Subtype.coind_bijective {α : Sort u_4} {β : Sort u_5} {f : αβ} {p : βProp} (h : (a : α) → p (f a)) (hf : ) :
@[simp]
theorem Subtype.map_coe {α : Sort u_1} {β : Sort u_2} {p : αProp} {q : βProp} (f : αβ) (h : (a : α) → p aq (f a)) :
∀ (a : ), ↑(Subtype.map f h a) = f a
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.

Instances For
theorem Subtype.map_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p : αProp} {q : βProp} {r : γProp} {x : } (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) (fun a ha => l (f a) (h a ha)) x
theorem Subtype.map_id {α : Sort u_1} {p : αProp} {h : (a : α) → p ap (id a)} :
Subtype.map id h = id
theorem Subtype.map_injective {α : Sort u_1} {β : Sort u_2} {p : αProp} {q : βProp} {f : αβ} (h : (a : α) → p aq (f a)) (hf : ) :
theorem Subtype.map_involutive {α : Sort u_1} {p : αProp} {f : αα} (h : (a : α) → p ap (f a)) (hf : ) :
instance Subtype.instHasEquivSubtype {α : Sort u_1} [] (p : αProp) :
theorem Subtype.equiv_iff {α : Sort u_1} [] {p : αProp} {s : } {t : } :
s t s t
theorem Subtype.refl {α : Sort u_1} {p : αProp} [] (s : ) :
s s
theorem Subtype.symm {α : Sort u_1} {p : αProp} [] {s : } {t : } (h : s t) :
t s
theorem Subtype.trans {α : Sort u_1} {p : αProp} [] {s : } {t : } {u : } (h₁ : s t) (h₂ : t u) :
s u
theorem Subtype.equivalence {α : Sort u_1} [] (p : αProp) :
Equivalence HasEquiv.Equiv
instance Subtype.instSetoidSubtype {α : Sort u_1} [] (p : αProp) :

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 S