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

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.

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.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_4} {p : α → Prop} {q : β → Prop} {a : { x : α // p x }} {b : { y : β // q y }} (h : α = β) (h' : p ≍ q) : a ≍ b ↔ ↑a ≍ ↑b

@[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'

Restatement of Subtype.mk.injEq as an iff.

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 : Subtype p) => ↑a

@[simp]

theorem Subtype.val_injective {α : Sort u_1} {p : α → Prop} : Function.Injective 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 = ↑b ↔ a = b

theorem Subtype.coe_ne_coe {α : Sort u_1} {p : α → Prop} {a 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 = ⟨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

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⟩

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

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

@[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

theorem Subtype.restrict_def {α : Sort u_4} {β : Type u_5} (f : α → β) (p : α → Prop) : 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 (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) => restrict p f

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, ⋯⟩

@[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✝

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)

@[simp]

theorem Subtype.coind_injective_iff {α : Sort u_4} {β : Sort u_5} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) : Function.Injective (coind f h) ↔ Function.Injective 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 = ⟨f ↑x, ⋯⟩

@[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✝

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, ⋯⟩

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

theorem Subtype.map_id {α : Sort u_1} {p : α → Prop} {h : ∀ (a : α), p a → p (id a)} : 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 (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 (map f h)

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

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

@[instance_reducible]

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 }

theorem Subtype.equiv_iff {α : Sort u_1} [HasEquiv α] {p : α → Prop} {s 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 t : Subtype p} (h : s ≈ t) : t ≈ s

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 HasEquiv.Equiv

@[instance_reducible]

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.

@[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