Documentation

Mathlib.Data.Subtype

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 xProp} :
(∀ (x : α) (h : p x), q x h) ∀ (x : { a : α // p a }), q x (_ : p 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 xProp} :
(∃ (x : α), ∃ (h : p x), q x h) ∃ (x : { a : α // p a }), q x (_ : p 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) :
{ 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 := (_ : p b) }
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
Instances For
    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) :
    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
    Instances For
      theorem Subtype.coind_injective {α : Sort u_4} {β : Sort u_5} {f : αβ} {p : βProp} (h : ∀ (a : α), p (f a)) (hf : Function.Injective f) :
      theorem Subtype.coind_surjective {α : Sort u_4} {β : Sort u_5} {f : αβ} {p : βProp} (h : ∀ (a : α), p (f a)) (hf : Function.Surjective f) :
      theorem Subtype.coind_bijective {α : Sort u_4} {β : Sort u_5} {f : αβ} {p : βProp} (h : ∀ (a : α), p (f a)) (hf : Function.Bijective f) :
      @[simp]
      theorem Subtype.map_coe {α : Sort u_1} {β : Sort u_2} {p : αProp} {q : βProp} (f : αβ) (h : ∀ (a : α), p aq (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 aq (f a)) :

      Restriction of a function to a function on subtypes.

      Equations
      • Subtype.map f h x = { val := f x, property := (_ : q (f x)) }
      Instances For
        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 aq (f a)) (g : βγ) (l : ∀ (a : β), q ar (g a)) :
        Subtype.map g l (Subtype.map f h x) = Subtype.map (g f) (_ : ∀ (a : α), p ar (g (f a))) 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 : Function.Injective f) :
        theorem Subtype.map_involutive {α : Sort u_1} {p : αProp} {f : αα} (h : ∀ (a : α), p ap (f a)) (hf : Function.Involutive f) :
        instance Subtype.instHasEquivSubtype {α : Sort u_1} [HasEquiv α] (p : αProp) :
        Equations
        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) :
        Equations

        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