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

@[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 { val := a, property := b }

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.

theorem Subtype.ext {α : Sort u_1} {p : α → Prop} {a1 : { x : α // p x }} {a2 : { x : α // p x }} : ↑a1 = ↑a2 → a1 = 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 = ↑a2 → a1 = 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 := ⋯ }

theorem Subtype.coe_eq_iff {α : Sort u_1} {p : α → Prop} {a : { a : α // p a }} {b : α} : ↑a = b ↔ ∃ (h : p b), a = { val := b, property := h }

theorem Subtype.coe_injective {α : Sort u_1} {p : α → Prop} : Function.Injective fun (a : Subtype p) => ↑a

theorem Subtype.val_injective {α : Sort u_1} {p : α → Prop} : Function.Injective Subtype.val

theorem Subtype.coe_inj {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : Subtype p} : ↑a = ↑b ↔ a = b

theorem Subtype.val_inj {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : Subtype p} : ↑a = ↑b ↔ a = b

@[simp]

theorem exists_eq_subtype_mk_iff {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : α} : (∃ (h : p b), a = { val := b, property := h }) ↔ ↑a = b

@[simp]

theorem exists_subtype_mk_eq_iff {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : α} : (∃ (h : p b), { val := b, property := h } = a) ↔ b = ↑a

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

theorem Subtype.restrict_apply {α : Sort u_5} {β : α → Type u_4} (f : (x : α) → β x) (p : α → Prop) (x : Subtype p) : Subtype.restrict p f x = f ↑x

theorem Subtype.restrict_def {α : Sort u_4} {β : Type u_5} (f : α → β) (p : α → Prop) : Subtype.restrict p f = f ∘ fun (a : Subtype p) => ↑a

theorem Subtype.restrict_injective {α : Sort u_4} {β : Type u_5} {f : α → β} (p : α → Prop) (h : Function.Injective f) : Function.Injective (Subtype.restrict p f)

theorem Subtype.surjective_restrict {α : Sort u_5} {β : α → Type u_4} [ne : ∀ (a : α), Nonempty (β a)] (p : α → Prop) : Function.Surjective fun (f : (x : α) → β x) => Subtype.restrict p f

@[simp]

theorem Subtype.coind_coe {α : Sort u_4} {β : Sort u_5} (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)) : ∀ (a : α), ↑(Subtype.coind f h a) = f a

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 = { val := f a, property := ⋯ }

theorem Subtype.coind_injective {α : Sort u_4} {β : Sort u_5} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : Function.Injective f) : Function.Injective (Subtype.coind f h)

theorem Subtype.coind_surjective {α : Sort u_4} {β : Sort u_5} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : Function.Surjective f) : Function.Surjective (Subtype.coind f h)

theorem Subtype.coind_bijective {α : Sort u_4} {β : Sort u_5} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : Function.Bijective f) : Function.Bijective (Subtype.coind f h)

@[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), ↑(Subtype.map f h a) = f ↑a

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 = { val := f ↑x, property := ⋯ }

theorem Subtype.map_def {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a)) : Subtype.map f h = fun (x : { a : α // p a }) => { val := f ↑x, property := ⋯ }

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)) : 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 a → p (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 a → q (f a)) (hf : Function.Injective f) : Function.Injective (Subtype.map f h)

theorem Subtype.map_involutive {α : Sort u_1} {p : α → Prop} {f : α → α} (h : ∀ (a : α), p a → p (f a)) (hf : Function.Involutive f) : Function.Involutive (Subtype.map f h)

instance Subtype.instHasEquivSubtype {α : Sort u_1} [HasEquiv α] (p : α → Prop) : HasEquiv (Subtype p)

Equations

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

theorem Subtype.equiv_iff {α : Sort u_1} [HasEquiv α] {p : α → Prop} {s : Subtype p} {t : Subtype p} : s ≈ t ↔ ↑s ≈ ↑t

theorem Subtype.refl {α : Sort u_1} {p : α → Prop} [Setoid α] (s : Subtype p) : s ≈ s

theorem Subtype.symm {α : Sort u_1} {p : α → Prop} [Setoid α] {s : Subtype p} {t : Subtype p} (h : s ≈ t) : t ≈ s

theorem Subtype.trans {α : Sort u_1} {p : α → Prop} [Setoid α] {s : Subtype p} {t : Subtype p} {u : Subtype p} (h₁ : s ≈ t) (h₂ : t ≈ u) : s ≈ u

theorem Subtype.equivalence {α : Sort u_1} [Setoid α] (p : α → Prop) : Equivalence HasEquiv.Equiv

instance Subtype.instSetoidSubtype {α : Sort u_1} [Setoid α] (p : α → Prop) : Setoid (Subtype p)

Equations

• Subtype.instSetoidSubtype p = { r := fun (x x_1 : Subtype p) => 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