# 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 a, 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

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 : { a : α // p a }), q x) ∃ (a : α), ∃ (b : p a), q a, b
theorem Subtype.exists' {α : Sort u_1} {p : αProp} {q : (x : α) → p xProp} :
(∃ (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.

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) :
a, h = a
theorem Subtype.coe_mk {α : Sort u_1} {p : αProp} (a : α) (h : p a) :
a, h = a
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} :
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
theorem Subtype.coe_ne_coe {α : Sort u_1} {p : αProp} {a : } {b : } :
a b a b
@[deprecated Subtype.coe_ne_coe]
theorem Subtype.ne_of_val_ne {α : Sort u_1} {p : αProp} {a : } {b : } :
a ba b

Alias of the forward direction of Subtype.coe_ne_coe.

@[simp]
theorem exists_eq_subtype_mk_iff {α : Sort u_1} {p : αProp} {a : } {b : α} :
(∃ (h : p b), a = b, h) a = b
@[simp]
theorem exists_subtype_mk_eq_iff {α : Sort u_1} {p : αProp} {a : } {b : α} :
(∃ (h : p b), b, 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

Equations
• = f x
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) :
Function.Surjective fun (f : (x : α) → β x) =>
@[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

Equations
• = f a,
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.

Equations
Instances For
theorem Subtype.map_def {α : Sort u_1} {β : Sort u_2} {p : αProp} {q : βProp} (f : αβ) (h : ∀ (a : α), p aq (f a)) :
= fun (x : { a : α // p a }) => f x,
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) 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.instHasEquiv_mathlib {α : Sort u_1} [] (p : αProp) :
Equations
• = { Equiv := fun (s t : ) => s t }
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.instSetoid_mathlib {α : Sort u_1} [] (p : αProp) :
Equations
• = { r := fun (x x_1 : ) => x x_1, iseqv := }

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