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

source
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 `Mathlib/Data/Set/Basic.lean`.

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

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

source
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
source
theorem Subtype.heq_iff_coe_heq {α β : Sort u_4} {p : α → Prop} {q : β → Prop} {a : { x : α // p x }} {b : { y : β // q y }} (h : α = β) (h' : p ≍ q) :
a ≍ b ↔ ↑a ≍ ↑b
source
@[deprecated Subtype.ext (since := "2025-09-10")]
theorem Subtype.ext_val {α : Sort u_1} {p : α → Prop} {a1 a2 : { x : α // p x }} :
↑a1 = ↑a2 → a1 = a2
source
@[deprecated Subtype.ext_iff (since := "2025-09-10")]
theorem Subtype.ext_iff_val {α : Sort u_1} {p : α → Prop} {a1 a2 : { x : α // p x }} :
a1 = a2 ↔ ↑a1 = ↑a2
source
@[simp]
theorem Subtype.coe_eta {α : Sort u_1} {p : α → Prop} (a : { a : α // p a }) (h : p ↑a) :
⟨↑a, h⟩ = a
source
theorem Subtype.coe_mk {α : Sort u_1} {p : α → Prop} (a : α) (h : p a) :
↑⟨a, h⟩ = a
source
theorem Subtype.mk_eq_mk {α : Sort u_1} {p : α → Prop} {a : α} {h : p a} {a' : α} {h' : p a'} :
⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'

Restatement of `Subtype.mk.injEq` as an iff.

source
theorem Subtype.coe_eq_of_eq_mk {α : Sort u_1} {p : α → Prop} {a : { a : α // p a }} {b : α} (h : ↑a = b) :
a = ⟨b, ⋯⟩
source
theorem Subtype.coe_eq_iff {α : Sort u_1} {p : α → Prop} {a : { a : α // p a }} {b : α} :
↑a = b ↔ ∃ (h : p b), a = ⟨b, h⟩
source
theorem Subtype.coe_injective {α : Sort u_1} {p : α → Prop} :
Function.Injective fun (a : Subtype p) => ↑a
source
@[simp]
theorem Subtype.val_injective {α : Sort u_1} {p : α → Prop} :
Function.Injective val
source
theorem Subtype.coe_inj {α : Sort u_1} {p : α → Prop} {a b : Subtype p} :
↑a = ↑b ↔ a = b
source
theorem Subtype.val_inj {α : Sort u_1} {p : α → Prop} {a b : Subtype p} :
↑a = ↑b ↔ a = b
source
theorem Subtype.coe_ne_coe {α : Sort u_1} {p : α → Prop} {a b : Subtype p} :
↑a ≠ ↑b ↔ a ≠ b
source
@[simp]
theorem exists_eq_subtype_mk_iff {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : α} :
(∃ (h : p b), a = ⟨b, h⟩) ↔ ↑a = b
source
@[simp]
theorem exists_subtype_mk_eq_iff {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : α} :
(∃ (h : p b), ⟨b, h⟩ = a) ↔ b = ↑a
source
theorem Function.extend_val_apply {β : Sort u_2} {γ : Sort u_3} {p : β → Prop} {g : { x : β // p x } → γ} {j : β → γ} {b : β} (hb : p b) :
extend Subtype.val g j b = g ⟨b, hb⟩
source
theorem Function.extend_val_apply' {β : Sort u_2} {γ : Sort u_3} {p : β → Prop} {g : { x : β // p x } → γ} {j : β → γ} {b : β} (hb : ¬p b) :
extend Subtype.val g j b = j b
source
def Subtype.restrict {α : Sort u_5} {β : α → Type u_4} (p : α → Prop) (f : (x : α) → β x) (x : Subtype p) :
β ↑x

Restrict a (dependent) function to a subtype

Equations

- Subtype.restrict p f x = f ↑x

Instances For

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

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

Equations

- Subtype.coind f h a = ⟨f a, ⋯⟩

Instances For

source
@[simp]
theorem Subtype.coind_coe {α : Sort u_4} {β : Sort u_5} (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)) (a✝ : α) :
↑(coind f h a✝) = f a✝
source
theorem Subtype.coind_injective {α : Sort u_4} {β : Sort u_5} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : Function.Injective f) :
Function.Injective (coind f h)
source
def Subtype.map {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a)) :
Subtype p → Subtype q

Restriction of a function to a function on subtypes.

Equations

- Subtype.map f h x = ⟨f ↑x, ⋯⟩

Instances For

source
@[simp]
theorem Subtype.map_coe {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a)) (a✝ : Subtype p) :
↑(map f h a✝) = f ↑a✝
source
theorem Subtype.map_def {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a)) :
map f h = fun (x : Subtype p) => ⟨f ↑x, ⋯⟩
source
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 a → q (f a)) (g : β → γ) (l : ∀ (a : β), q a → r (g a)) :
map g l (map f h x) = map (g ∘ f) ⋯ x
source
theorem Subtype.map_id {α : Sort u_1} {p : α → Prop} {h : ∀ (a : α), p a → p (id a)} :
map id h = id
source
theorem Subtype.map_injective {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ (a : α), p a → q (f a)) (hf : Function.Injective f) :
Function.Injective (map f h)
source
theorem Subtype.map_involutive {α : Sort u_1} {p : α → Prop} {f : α → α} (h : ∀ (a : α), p a → p (f a)) (hf : Function.Involutive f) :
Function.Involutive (map f h)
source
theorem Subtype.map_eq {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f g : α → β} (h₁ : ∀ (a : α), p a → q (f a)) (h₂ : ∀ (a : α), p a → q (g a)) {x y : Subtype p} :
map f h₁ x = map g h₂ y ↔ f ↑x = g ↑y
source
theorem Subtype.map_ne {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f g : α → β} (h₁ : ∀ (a : α), p a → q (f a)) (h₂ : ∀ (a : α), p a → q (g a)) {x y : Subtype p} :
map f h₁ x ≠ map g h₂ y ↔ f ↑x ≠ g ↑y
source
instance Subtype.instHasEquiv_mathlib {α : Sort u_1} [HasEquiv α] (p : α → Prop) :
HasEquiv (Subtype p)
Equations

- Subtype.instHasEquiv_mathlib p = { Equiv := fun (s t : Subtype p) => ↑s ≈ ↑t }

source
theorem Subtype.equiv_iff {α : Sort u_1} [HasEquiv α] {p : α → Prop} {s t : Subtype p} :
s ≈ t ↔ ↑s ≈ ↑t
source
theorem Subtype.refl {α : Sort u_1} {p : α → Prop} [Setoid α] (s : Subtype p) :
s ≈ s
source
theorem Subtype.symm {α : Sort u_1} {p : α → Prop} [Setoid α] {s t : Subtype p} (h : s ≈ t) :
t ≈ s
source
theorem Subtype.trans {α : Sort u_1} {p : α → Prop} [Setoid α] {s t u : Subtype p} (h₁ : s ≈ t) (h₂ : t ≈ u) :
s ≈ u
source
theorem Subtype.equivalence {α : Sort u_1} [Setoid α] (p : α → Prop) :
Equivalence HasEquiv.Equiv
source
instance Subtype.instSetoid_mathlib {α : Sort u_1} [Setoid α] (p : α → Prop) :
Setoid (Subtype p)
Equations

- Subtype.instSetoid_mathlib p = { r := fun (x1 x2 : Subtype p) => x1 ≈ x2, iseqv := ⋯ }

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

source
@[simp]
theorem Subtype.coe_prop {α : Type u_1} {S : Set α} (a : { a : α // a ∈ S }) :
↑a ∈ S
source
theorem Subtype.val_prop {α : Type u_1} {S : Set α} (a : { a : α // a ∈ S }) :
↑a ∈ S