mathlib3 documentation

data.subtype

Subtypes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

subtype.simps.coe x = ↑x

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

@[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 = ↑a2 → a1 = 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.val → a1 = 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} :

function.injective coe

theorem subtype.val_injective {α : Sort u_1} {p : α → Prop} :

function.injective subtype.val

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

subtype.restrict p f x = f ↑x

theorem subtype.restrict_apply {α : Sort u_1} {β : α → Type u_2} (f : Π (x : α), β x) (p : α → Prop) (x : subtype p) :

subtype.restrict p f x = f x.val

theorem subtype.restrict_def {α : Sort u_1} {β : Type u_2} (f : α → β) (p : α → Prop) :

subtype.restrict p f = f ∘ coe

theorem subtype.restrict_injective {α : Sort u_1} {β : Type u_2} {f : α → β} (p : α → Prop) (h : function.injective f) :

function.injective (subtype.restrict p 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

subtype.coind f h = λ (a : α), ⟨f a, _⟩

theorem subtype.coind_injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : function.injective f) :

function.injective (subtype.coind f h)

theorem subtype.coind_surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : function.surjective f) :

function.surjective (subtype.coind f h)

theorem subtype.coind_bijective {α : Sort u_1} {β : Sort u_2} {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)) (ᾰ : subtype p) :

↑(subtype.map f h ᾰ) = f ↑ᾰ

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 : subtype p), ⟨f ↑x, _⟩

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)

@[protected, instance]

def subtype.has_equiv {α : Sort u_1} [has_equiv α] (p : α → Prop) :

has_equiv (subtype p)

Equations

subtype.has_equiv p = {equiv := λ (s t : subtype p), ↑s ≈ ↑t}

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

equivalence has_equiv.equiv

@[protected, instance]

def subtype.setoid {α : Sort u_1} [setoid α] (p : α → Prop) :

setoid (subtype p)

Equations

subtype.setoid p = {r := has_equiv.equiv (subtype.has_equiv p), 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}) :

theorem subtype.val_prop {α : Type u_1} {S : set α} (a : {a // a ∈ S}) :