Mathlib.Data.Subtype

Subtype.prop theorem

(x : Subtype p) : p x

Full source

/-- 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`. -/
theorem prop (x : Subtype p) : p x :=
  x.2

Property Holds for Subtype Elements

Informal description

For any element $x$ of the subtype $\{a : \alpha \mid p(a)\}$, the property $p$ holds for the underlying value of $x$.

Subtype.forall' theorem

{q : ∀ x, p x → Prop} : (∀ x h, q x h) ↔ ∀ x : { a // p a }, q x x.2

Full source

/-- 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 theorem forall' {q : ∀ x, p x → Prop} : (∀ x h, q x h) ↔ ∀ x : { a // p a }, q x x.2 :=
  (@Subtype.forall _ _ fun x ↦ q x.1 x.2).symm

Universal Quantification over Subtypes vs. Pairs

Informal description

Let $p : \alpha \to \mathrm{Prop}$ be a predicate on a type $\alpha$, and let $q : \forall x, p x \to \mathrm{Prop}$ be a dependent predicate. Then the following are equivalent: 1. For all $x \in \alpha$ and all proofs $h$ that $p x$ holds, $q x h$ holds. 2. For all elements $x$ of the subtype $\{a \in \alpha \mid p a\}$, $q x x.2$ holds (where $x.2$ is the proof that $p x$ holds).

Subtype.exists' theorem

{q : ∀ x, p x → Prop} : (∃ x h, q x h) ↔ ∃ x : { a // p a }, q x x.2

Full source

/-- 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 theorem exists' {q : ∀ x, p x → Prop} : (∃ x h, q x h) ↔ ∃ x : { a // p a }, q x x.2 :=
  (@Subtype.exists _ _ fun x ↦ q x.1 x.2).symm

Existence in Subtypes via Existential Quantifier

Informal description

Let $p : \alpha \to \mathrm{Prop}$ be a predicate on a type $\alpha$, and let $q$ be a predicate on pairs $(x, h)$ where $x \in \alpha$ and $h : p(x)$. Then the following are equivalent: 1. There exists $x \in \alpha$ and $h : p(x)$ such that $q(x, h)$ holds. 2. There exists an element $x$ of the subtype $\{a \in \alpha \mid p(a)\}$ such that $q(x, x.2)$ holds, where $x.2$ is the proof that $p(x)$ holds.

Subtype.heq_iff_coe_eq theorem

(h : ∀ x, p x ↔ q x) {a1 : { x // p x }} {a2 : { x // q x }} : HEq a1 a2 ↔ (a1 : α) = (a2 : α)

Full source

theorem heq_iff_coe_eq (h : ∀ x, p x ↔ q x) {a1 : { x // p x }} {a2 : { x // q x }} :
    HEqHEq a1 a2 ↔ (a1 : α) = (a2 : α) :=
  Eq.rec
    (motive := fun (pp : (α → Prop)) _ ↦ ∀ a2' : {x // pp x}, HEqHEq a1 a2' ↔ (a1 : α) = (a2' : α))
    (fun _ ↦ heq_iff_eq.trans Subtype.ext_iff) (funext <| fun x ↦ propext (h x)) a2

Heterogeneous Equality of Subtypes via Underlying Value Equality

Informal description

Let $p$ and $q$ be predicates on a type $\alpha$, and suppose that for all $x \in \alpha$, $p(x) \leftrightarrow q(x)$. For any elements $a_1 \in \{x \in \alpha \mid p(x)\}$ and $a_2 \in \{x \in \alpha \mid q(x)\}$, the following are equivalent: 1. $a_1$ and $a_2$ are heterogeneous equal (HEq) 2. The underlying values of $a_1$ and $a_2$ in $\alpha$ are equal (i.e., $(a_1 : \alpha) = (a_2 : \alpha)$).

Subtype.heq_iff_coe_heq theorem

 {α β : Sort _} {p : α → Prop} {q : β → Prop} {a : { x // p x }} {b : { y // q y }} (h : α = β) (h' : HEq p q) :
  HEq a b ↔ HEq (a : α) (b : β)

Full source

lemma heq_iff_coe_heq {α β : Sort _} {p : α → Prop} {q : β → Prop} {a : {x // p x}}
    {b : {y // q y}} (h : α = β) (h' : HEq p q) : HEqHEq a b ↔ HEq (a : α) (b : β) := by
  subst h
  subst h'
  rw [heq_iff_eq, heq_iff_eq, Subtype.ext_iff]

Heterogeneous Equality of Subtypes via Underlying Values

Informal description

Let $\alpha$ and $\beta$ be types, with predicates $p : \alpha \to \text{Prop}$ and $q : \beta \to \text{Prop}$. Given elements $a : \{x // p x\}$ and $b : \{y // q y\}$, and assuming $\alpha = \beta$ and that $p$ and $q$ are heterogeneously equal (denoted $\text{HEq}\, p\, q$), then the elements $a$ and $b$ are heterogeneously equal if and only if their underlying values (of types $\alpha$ and $\beta$ respectively) are heterogeneously equal. In symbols: \[ \text{HEq}\, a\, b \leftrightarrow \text{HEq}\, (a : \alpha)\, (b : \beta) \]

Subtype.ext_val theorem

{a1 a2 : { x // p x }} : a1.1 = a2.1 → a1 = a2

Full source

theorem ext_val {a1 a2 : { x // p x }} : a1.1 = a2.1 → a1 = a2 :=
  Subtype.ext

Equality of Subtypes via Underlying Values

Informal description

For any two elements $a_1$ and $a_2$ of a subtype $\{x : \alpha \mid p(x)\}$, if their underlying values (of type $\alpha$) are equal, then $a_1$ and $a_2$ are equal as elements of the subtype.

Subtype.ext_iff_val theorem

{a1 a2 : { x // p x }} : a1 = a2 ↔ a1.1 = a2.1

Full source

theorem ext_iff_val {a1 a2 : { x // p x }} : a1 = a2 ↔ a1.1 = a2.1 :=
  Subtype.ext_iff

Equality Criterion for Subtypes via Underlying Values

Informal description

For any two elements $a_1$ and $a_2$ of a subtype $\{x : \alpha \mid p(x)\}$, the elements are equal if and only if their underlying values (of type $\alpha$) are equal. That is, $a_1 = a_2 \leftrightarrow a_1.1 = a_2.1$.

Subtype.coe_eta theorem

(a : { a // p a }) (h : p a) : mk (↑a) h = a

Full source

@[simp]
theorem coe_eta (a : { a // p a }) (h : p a) : mk (↑a) h = a :=
  Subtype.ext rfl

Eta Reduction for Subtype Elements

Informal description

For any element $a$ of the subtype $\{a : \alpha \mid p(a)\}$ and any proof $h$ that $p(a)$ holds, the constructed term $\langle a, h \rangle$ is equal to $a$ when viewed as an element of the subtype.

Subtype.coe_mk theorem

(a h) : (@mk α p a h : α) = a

Full source

theorem coe_mk (a h) : (@mk α p a h : α) = a :=
  rfl

Subtype Coercion of Constructed Element Equals Original Element

Informal description

For any element $a$ of type $\alpha$ and a proof $h$ that $a$ satisfies the predicate $p$, the coercion of the subtype element $\langle a, h \rangle$ back to $\alpha$ equals $a$. In other words, $(\langle a, h \rangle : \alpha) = a$.

Subtype.mk_eq_mk theorem

{a h a' h'} : @mk α p a h = @mk α p a' h' ↔ a = a'

Full source

/-- Restatement of `subtype.mk.injEq` as an iff. -/
theorem mk_eq_mk {a h a' h'} : @mk α p a h = @mk α p a' h' ↔ a = a' := by simp

Equality of Subtype Elements iff Underlying Values Are Equal

Informal description

For any type $\alpha$ with a predicate $p : \alpha \to \mathrm{Prop}$, and elements $a, a' \in \alpha$ with proofs $h : p(a)$ and $h' : p(a')$, the equality $\langle a, h \rangle = \langle a', h' \rangle$ holds if and only if $a = a'$.

Subtype.coe_eq_of_eq_mk theorem

{a : { a // p a }} {b : α} (h : ↑a = b) : a = ⟨b, h ▸ a.2⟩

Full source

theorem coe_eq_of_eq_mk {a : { a // p a }} {b : α} (h : ↑a = b) : a = ⟨b, h ▸ a.2⟩ :=
  Subtype.ext h

Subtype Equality from Coercion Equality

Informal description

Let $a$ be an element of the subtype $\{a : \alpha \mid p(a)\}$ and $b$ an element of $\alpha$. If the coercion of $a$ to $\alpha$ equals $b$ (i.e., $\uparrow a = b$), then $a$ is equal to the subtype element $\langle b, h \rangle$, where $h$ is the proof that $p(b)$ holds obtained by substituting $b$ for $\uparrow a$ in the proof that $p(\uparrow a)$ holds.

Subtype.coe_eq_iff theorem

{a : { a // p a }} {b : α} : ↑a = b ↔ ∃ h, a = ⟨b, h⟩

Full source

theorem coe_eq_iff {a : { a // p a }} {b : α} : ↑a = b ↔ ∃ h, a = ⟨b, h⟩ :=
  ⟨fun h ↦ h ▸ ⟨a.2, (coe_eta _ _).symm⟩, fun ⟨_, ha⟩ ↦ ha.symm ▸ rfl⟩

Subtype Coercion Equality Characterization: $\uparrow a = b \leftrightarrow \exists h, a = \langle b, h \rangle$

Informal description

For an element $a$ of the subtype $\{a : \alpha \mid p(a)\}$ and an element $b$ of $\alpha$, the coercion of $a$ to $\alpha$ equals $b$ if and only if there exists a proof $h$ that $p(b)$ holds such that $a$ is equal to the subtype element $\langle b, h \rangle$.

Subtype.coe_injective theorem

: Injective (fun (a : Subtype p) ↦ (a : α))

Full source

theorem coe_injective : Injective (fun (a : Subtype p) ↦ (a : α)) := fun _ _ ↦ Subtype.ext

Injectivity of Subtype Coercion

Informal description

The canonical embedding from a subtype $\{a : \alpha \mid p(a)\}$ to its parent type $\alpha$ (given by the coercion function $(a : \text{Subtype } p) \mapsto (a : \alpha)$) is injective. In other words, if two elements of the subtype have equal values in $\alpha$, then they are equal in the subtype.

Subtype.val_injective theorem

: Injective (@val _ p)

Full source

@[simp] theorem val_injective : Injective (@val _ p) :=
  coe_injective

Injectivity of Subtype Projection

Informal description

The function `val` that projects an element of a subtype $\{x : \alpha \mid p(x)\}$ to its underlying value in $\alpha$ is injective. That is, for any two elements $a, b$ in the subtype, if $a.val = b.val$, then $a = b$.

Subtype.coe_inj theorem

{a b : Subtype p} : (a : α) = b ↔ a = b

Full source

theorem coe_inj {a b : Subtype p} : (a : α) = b ↔ a = b :=
  coe_injective.eq_iff

Equality in Subtype via Parent Type Equality

Informal description

For any two elements $a$ and $b$ of a subtype $\{x : \alpha \mid p(x)\}$, the values of $a$ and $b$ in the parent type $\alpha$ are equal if and only if $a$ and $b$ are equal in the subtype.

Subtype.val_inj theorem

{a b : Subtype p} : a.val = b.val ↔ a = b

Full source

theorem val_inj {a b : Subtype p} : a.val = b.val ↔ a = b :=
  coe_inj

Equivalence of Subtype Equality via Underlying Value Equality

Informal description

For any two elements $a$ and $b$ of a subtype $\{x : \alpha \mid p(x)\}$, the underlying values $a.val$ and $b.val$ in the parent type $\alpha$ are equal if and only if $a$ and $b$ are equal in the subtype.

Subtype.coe_ne_coe theorem

{a b : Subtype p} : (a : α) ≠ b ↔ a ≠ b

Full source

lemma coe_ne_coe {a b : Subtype p} : (a : α) ≠ b(a : α) ≠ b ↔ a ≠ b := coe_injective.ne_iff

Inequality in Subtype via Parent Type Inequality

Informal description

For any two elements $a$ and $b$ of a subtype $\{x : \alpha \mid p(x)\}$, the values of $a$ and $b$ in the parent type $\alpha$ are not equal if and only if $a$ and $b$ are not equal in the subtype.

exists_eq_subtype_mk_iff theorem

{a : Subtype p} {b : α} : (∃ h : p b, a = Subtype.mk b h) ↔ ↑a = b

Full source

@[simp]
theorem _root_.exists_eq_subtype_mk_iff {a : Subtype p} {b : α} :
    (∃ h : p b, a = Subtype.mk b h) ↔ ↑a = b :=
  coe_eq_iff.symm

Subtype Construction Equivalence: $(\exists h, a = \langle b, h \rangle) \leftrightarrow \uparrow a = b$

Informal description

For an element $a$ of the subtype $\{x : \alpha \mid p(x)\}$ and an element $b$ of $\alpha$, there exists a proof $h$ that $p(b)$ holds and $a$ equals the subtype element $\langle b, h \rangle$ if and only if the coercion of $a$ to $\alpha$ equals $b$.

exists_subtype_mk_eq_iff theorem

{a : Subtype p} {b : α} : (∃ h : p b, Subtype.mk b h = a) ↔ b = a

Full source

@[simp]
theorem _root_.exists_subtype_mk_eq_iff {a : Subtype p} {b : α} :
    (∃ h : p b, Subtype.mk b h = a) ↔ b = a := by
  simp only [@eq_comm _ b, exists_eq_subtype_mk_iff, @eq_comm _ _ a]

Existence of Subtype Construction Equivalence: $(\exists h, \text{Subtype.mk } b h = a) \leftrightarrow b = a$

Informal description

For a subtype $\{x : \alpha \mid p(x)\}$ and elements $a$ of this subtype and $b$ of type $\alpha$, there exists a proof $h$ that $p(b)$ holds and that the subtype element constructed from $b$ and $h$ equals $a$ if and only if $b$ equals the underlying value of $a$.

Function.extend_val_apply theorem

{p : β → Prop} {g : { x // p x } → γ} {j : β → γ} {b : β} (hb : p b) : val.extend g j b = g ⟨b, hb⟩

Full source

theorem _root_.Function.extend_val_apply {p : β → Prop} {g : {x // p x} → γ} {j : β → γ}
    {b : β} (hb : p b) : val.extend g j b = g ⟨b, hb⟩ :=
  val_injective.extend_apply g j ⟨b, hb⟩

Extension of Subtype Function Evaluates to $g$ When Predicate Holds: $\text{val.extend}\,g\,j\,b = g(\langle b, hb \rangle)$ for $p(b)$

Informal description

For any predicate $p$ on a type $\beta$, functions $g : \{x \in \beta \mid p(x)\} \to \gamma$ and $j : \beta \to \gamma$, and any element $b \in \beta$ such that $p(b)$ holds, the extension of $g$ along the canonical projection $\text{val}$ with default function $j$ satisfies $\text{val.extend}\,g\,j\,b = g(\langle b, hb \rangle)$, where $hb$ is a proof that $p(b)$ holds.

Function.extend_val_apply' theorem

{p : β → Prop} {g : { x // p x } → γ} {j : β → γ} {b : β} (hb : ¬p b) : val.extend g j b = j b

Full source

theorem _root_.Function.extend_val_apply' {p : β → Prop} {g : {x // p x} → γ} {j : β → γ}
    {b : β} (hb : ¬ p b) : val.extend g j b = j b := by
  refine Function.extend_apply' g j b ?_
  rintro ⟨a, rfl⟩
  exact hb a.2

Extension of Subtype Function Evaluates to Default When Predicate Fails: $\text{val.extend}\,g\,j\,b = j(b)$ when $\neg p(b)$

Informal description

For any predicate $p$ on a type $\beta$, functions $g : \{x \in \beta \mid p(x)\} \to \gamma$ and $j : \beta \to \gamma$, and any element $b \in \beta$ such that $\neg p(b)$ holds, the extension of $g$ along the canonical projection $\text{val}$ with default function $j$ satisfies $\text{val.extend}\,g\,j\,b = j(b)$.

Subtype.restrict definition

{α} {β : α → Type*} (p : α → Prop) (f : ∀ x, β x) (x : Subtype p) : β x.1

Full source

/-- Restrict a (dependent) function to a subtype -/
def restrict {α} {β : α → Type*} (p : α → Prop) (f : ∀ x, β x) (x : Subtype p) : β x.1 :=
  f x

Restriction of a dependent function to a subtype

Informal description

Given a predicate $p$ on a type $\alpha$ and a dependent function $f$ defined for all elements of $\alpha$, the restriction of $f$ to the subtype $\{x \in \alpha \mid p(x)\}$ is the function that maps each element $\langle x, h_x \rangle$ of the subtype to $f(x)$, where $h_x$ is a proof that $p(x)$ holds.

Subtype.restrict_apply theorem

{α} {β : α → Type*} (f : ∀ x, β x) (p : α → Prop) (x : Subtype p) : restrict p f x = f x.1

Full source

theorem restrict_apply {α} {β : α → Type*} (f : ∀ x, β x) (p : α → Prop) (x : Subtype p) :
    restrict p f x = f x.1 := by
  rfl

Restriction of a Function to a Subtype Evaluates as Original Function

Informal description

For any type $\alpha$, a dependent type family $\beta$ on $\alpha$, a function $f$ defined for all $x \in \alpha$ with values in $\beta(x)$, and a predicate $p$ on $\alpha$, the restriction of $f$ to the subtype $\{x \in \alpha \mid p(x)\}$ satisfies that for any element $x$ of the subtype, $(f \restriction p)(x) = f(x.1)$, where $x.1$ is the underlying element of $\alpha$.

Subtype.restrict_def theorem

{α β} (f : α → β) (p : α → Prop) : restrict p f = f ∘ (fun (a : Subtype p) ↦ a)

Full source

theorem restrict_def {α β} (f : α → β) (p : α → Prop) :
    restrict p f = f ∘ (fun (a : Subtype p) ↦ a) := rfl

Definition of Restriction via Subtype Projection

Informal description

For any function $f \colon \alpha \to \beta$ and predicate $p \colon \alpha \to \mathrm{Prop}$, the restriction of $f$ to the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the composition of $f$ with the canonical projection from the subtype to $\alpha$. That is, $\mathrm{restrict}\,p\,f = f \circ (\lambda a \colon \{x \in \alpha \mid p(x)\}, a.1)$.

Subtype.restrict_injective theorem

{α β} {f : α → β} (p : α → Prop) (h : Injective f) : Injective (restrict p f)

Full source

theorem restrict_injective {α β} {f : α → β} (p : α → Prop) (h : Injective f) :
    Injective (restrict p f) :=
  h.comp coe_injective

Injectivity of Function Restriction to Subtype

Informal description

For any function $f \colon \alpha \to \beta$ and predicate $p \colon \alpha \to \mathrm{Prop}$, if $f$ is injective, then the restriction of $f$ to the subtype $\{x \in \alpha \mid p(x)\}$ is also injective.

Subtype.surjective_restrict theorem

 {α} {β : α → Type*} [ne : ∀ a, Nonempty (β a)] (p : α → Prop) : Surjective fun f : ∀ x, β x ↦ restrict p f

Full source

theorem surjective_restrict {α} {β : α → Type*} [ne : ∀ a, Nonempty (β a)] (p : α → Prop) :
    Surjective fun f : ∀ x, β x ↦ restrict p f := by
  letI := Classical.decPred p
  refine fun f ↦ ⟨fun x ↦ if h : p x then f ⟨x, h⟩ else Nonempty.some (ne x), funext <| ?_⟩
  rintro ⟨x, hx⟩
  exact dif_pos hx

Surjectivity of Function Restriction to Subtype

Informal description

Let $\alpha$ be a type and $\beta : \alpha \to \text{Type}^*$ be a type family such that for each $a \in \alpha$, $\beta(a)$ is nonempty. For any predicate $p : \alpha \to \text{Prop}$, the restriction map that sends a dependent function $f : \forall x, \beta x$ to its restriction $\text{restrict}\ p\ f$ on the subtype $\{x \in \alpha \mid p(x)\}$ is surjective.

Subtype.coind definition

{α β} (f : α → β) {p : β → Prop} (h : ∀ a, p (f a)) : α → Subtype p

Full source

/-- Defining a map into a subtype, this can be seen as a "coinduction principle" of `Subtype` -/
@[simps]
def coind {α β} (f : α → β) {p : β → Prop} (h : ∀ a, p (f a)) : α → Subtype p := fun a ↦ ⟨f a, h a⟩

Coinduction into a subtype

Informal description

Given a function $f \colon \alpha \to \beta$ and a predicate $p \colon \beta \to \mathrm{Prop}$ such that $p(f(a))$ holds for all $a \in \alpha$, the function $\mathrm{coind}$ maps each $a \in \alpha$ to the pair $\langle f(a), h(a) \rangle$ in the subtype $\{y : \beta \mid p(y)\}$.

Subtype.coind_injective theorem

{α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Injective f) : Injective (coind f h)

Full source

theorem coind_injective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Injective f) :
    Injective (coind f h) := fun x y hxy ↦ hf <| by apply congr_arg Subtype.val hxy

Injectivity Preservation under Coinduction into Subtype

Informal description

Let $f \colon \alpha \to \beta$ be an injective function and $p \colon \beta \to \mathrm{Prop}$ a predicate such that $p(f(a))$ holds for all $a \in \alpha$. Then the function $\mathrm{coind}\,f\,h \colon \alpha \to \{y : \beta \mid p(y)\}$, defined by $\mathrm{coind}\,f\,h\,a = \langle f(a), h(a) \rangle$, is also injective.

Subtype.coind_surjective theorem

{α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Surjective f) : Surjective (coind f h)

Full source

theorem coind_surjective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Surjective f) :
    Surjective (coind f h) := fun x ↦
  let ⟨a, ha⟩ := hf x
  ⟨a, coe_injective ha⟩

Surjectivity Preservation under Coinduction into Subtype

Informal description

Let $f \colon \alpha \to \beta$ be a surjective function and $p \colon \beta \to \mathrm{Prop}$ a predicate such that $p(f(a))$ holds for all $a \in \alpha$. Then the function $\mathrm{coind}\,f\,h \colon \alpha \to \{y : \beta \mid p(y)\}$, defined by $\mathrm{coind}\,f\,h\,a = \langle f(a), h(a) \rangle$, is also surjective.

Subtype.coind_bijective theorem

{α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Bijective f) : Bijective (coind f h)

Full source

theorem coind_bijective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Bijective f) :
    Bijective (coind f h) :=
  ⟨coind_injective h hf.1, coind_surjective h hf.2⟩

Bijectivity Preservation under Coinduction into Subtype

Informal description

Let $f \colon \alpha \to \beta$ be a bijective function and $p \colon \beta \to \mathrm{Prop}$ a predicate such that $p(f(a))$ holds for all $a \in \alpha$. Then the function $\mathrm{coind}\,f\,h \colon \alpha \to \{y : \beta \mid p(y)\}$, defined by $\mathrm{coind}\,f\,h\,a = \langle f(a), h(a) \rangle$, is also bijective.

Subtype.map definition

{p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ a, p a → q (f a)) : Subtype p → Subtype q

Full source

/-- Restriction of a function to a function on subtypes. -/
@[simps]
def map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ a, p a → q (f a)) :
    Subtype p → Subtype q :=
  fun x ↦ ⟨f x, h x x.prop⟩

Restriction of a function to subtypes

Informal description

Given a function $f : \alpha \to \beta$ and predicates $p : \alpha \to \text{Prop}$, $q : \beta \to \text{Prop}$, the function `Subtype.map` restricts $f$ to a function from the subtype $\{x : \alpha \mid p x\}$ to the subtype $\{y : \beta \mid q y\}$, provided that for every $a \in \alpha$ satisfying $p a$, the image $f a$ satisfies $q (f a)$. Concretely, for $\langle x, h_x \rangle$ in the subtype $\{x : \alpha \mid p x\}$, where $h_x$ is a proof that $p x$ holds, the function returns $\langle f x, h x h_x \rangle$ in the subtype $\{y : \beta \mid q y\}$.

Subtype.map_def theorem

 {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ a, p a → q (f a)) : map f h = fun x ↦ ⟨f x, h x x.prop⟩

Full source

theorem map_def {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ a, p a → q (f a)) :
    map f h = fun x ↦ ⟨f x, h x x.prop⟩ :=
  rfl

Definition of Subtype Restriction via Mapping

Informal description

Given a function $f \colon \alpha \to \beta$ and predicates $p \colon \alpha \to \text{Prop}$, $q \colon \beta \to \text{Prop}$, the restricted function $\text{map}\,f\,h$ from the subtype $\{x \colon \alpha \mid p\,x\}$ to the subtype $\{y \colon \beta \mid q\,y\}$ (where $h$ ensures that $f$ preserves the predicates) is equal to the function that maps each element $\langle x, h_x \rangle$ to $\langle f\,x, h\,x\,h_x \rangle$.

Subtype.map_comp theorem

 {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) (fun a ha ↦ l (f a) <| h a ha) x

Full source

theorem map_comp {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) (fun a ha ↦ l (f a) <| h a ha) x :=
  rfl

Composition of Restricted Maps on Subtypes

Informal description

Let $p : \alpha \to \text{Prop}$, $q : \beta \to \text{Prop}$, and $r : \gamma \to \text{Prop}$ be predicates on types $\alpha$, $\beta$, and $\gamma$ respectively. Given functions $f : \alpha \to \beta$ and $g : \beta \to \gamma$ such that: 1. For all $a \in \alpha$, if $p(a)$ holds then $q(f(a))$ holds (witnessed by $h$), 2. For all $a \in \beta$, if $q(a)$ holds then $r(g(a))$ holds (witnessed by $l$), then for any $x \in \{x : \alpha \mid p(x)\}$, the composition of the restricted maps satisfies: \[ \text{map}\,g\,l\,(\text{map}\,f\,h\,x) = \text{map}\,(g \circ f)\,(\lambda a\,ha \mapsto l(f a)(h a ha))\,x \]

Subtype.map_id theorem

{p : α → Prop} {h : ∀ a, p a → p (id a)} : map (@id α) h = id

Full source

theorem map_id {p : α → Prop} {h : ∀ a, p a → p (id a)} : map (@id α) h = id :=
  funext fun _ ↦ rfl

Identity Function Preserves Subtype Predicate

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and proof $h$ that the identity function preserves $p$ (i.e., for all $a \in \alpha$, $p a$ implies $p (\text{id}\, a)$), the restricted identity function $\text{map}\,\text{id}\,h$ on the subtype $\{x : \alpha \mid p x\}$ is equal to the identity function on this subtype.

Subtype.map_injective theorem

 {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ a, p a → q (f a)) (hf : Injective f) : Injective (map f h)

Full source

theorem map_injective {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ a, p a → q (f a))
    (hf : Injective f) : Injective (map f h) :=
  coind_injective _ <| hf.comp coe_injective

Injectivity of Restricted Functions on Subtypes

Informal description

Let $p \colon \alpha \to \mathrm{Prop}$ and $q \colon \beta \to \mathrm{Prop}$ be predicates, and let $f \colon \alpha \to \beta$ be an injective function such that for every $a \in \alpha$, if $p(a)$ holds then $q(f(a))$ holds. Then the restricted function $\mathrm{map}\,f\,h \colon \{x \in \alpha \mid p(x)\} \to \{y \in \beta \mid q(y)\}$ is also injective.

Subtype.map_involutive theorem

{p : α → Prop} {f : α → α} (h : ∀ a, p a → p (f a)) (hf : Involutive f) : Involutive (map f h)

Full source

theorem map_involutive {p : α → Prop} {f : α → α} (h : ∀ a, p a → p (f a))
    (hf : Involutive f) : Involutive (map f h) :=
  fun x ↦ Subtype.ext (hf x)

Involutivity of Restricted Functions on Subtypes

Informal description

Let $f : \alpha \to \alpha$ be an involutive function (i.e., $f(f(x)) = x$ for all $x \in \alpha$) and let $p : \alpha \to \mathrm{Prop}$ be a predicate such that for every $a \in \alpha$, if $p(a)$ holds then $p(f(a))$ also holds. Then the restricted function $\mathrm{map}\, f\, h : \{x \in \alpha \mid p(x)\} \to \{x \in \alpha \mid p(x)\}$ is also involutive.

Subtype.instHasEquiv_mathlib instance

[HasEquiv α] (p : α → Prop) : HasEquiv (Subtype p)

Full source

instance [HasEquiv α] (p : α → Prop) : HasEquiv (Subtype p) :=
  ⟨fun s t ↦ (s : α) ≈ (t : α)⟩

Inheritance of Equivalence Relation on Subtypes

Informal description

For any type $\alpha$ equipped with an equivalence relation $\approx$ and any predicate $p : \alpha \to \mathrm{Prop}$, the subtype $\{x : \alpha \mid p x\}$ inherits an equivalence relation defined by $x \approx y$ for $x, y$ in the subtype if and only if $x \approx y$ holds in $\alpha$.

Subtype.equiv_iff theorem

[HasEquiv α] {p : α → Prop} {s t : Subtype p} : s ≈ t ↔ (s : α) ≈ (t : α)

Full source

theorem equiv_iff [HasEquiv α] {p : α → Prop} {s t : Subtype p} : s ≈ ts ≈ t ↔ (s : α) ≈ (t : α) :=
  Iff.rfl

Equivalence in Subtype iff Equivalence in Parent Type

Informal description

Let $\alpha$ be a type equipped with an equivalence relation $\approx$, and let $p : \alpha \to \mathrm{Prop}$ be a predicate. For any two elements $s, t$ of the subtype $\{x : \alpha \mid p x\}$, we have $s \approx t$ if and only if their underlying values in $\alpha$ satisfy $(s : \alpha) \approx (t : \alpha)$.

Subtype.refl theorem

(s : Subtype p) : s ≈ s

Full source

protected theorem refl (s : Subtype p) : s ≈ s :=
  Setoid.refl _

Reflexivity of Equivalence Relation on Subtypes

Informal description

For any element $s$ of a subtype $\{x : \alpha \mid p x\}$, the equivalence relation $\approx$ holds reflexively, i.e., $s \approx s$.

Subtype.symm theorem

{s t : Subtype p} (h : s ≈ t) : t ≈ s

Full source

protected theorem symm {s t : Subtype p} (h : s ≈ t) : t ≈ s :=
  Setoid.symm h

Symmetry of Equivalence Relation on Subtypes

Informal description

For any type $\alpha$ with an equivalence relation $\approx$ and any predicate $p : \alpha \to \mathrm{Prop}$, if two elements $s$ and $t$ of the subtype $\{x : \alpha \mid p x\}$ satisfy $s \approx t$, then $t \approx s$.

Subtype.trans theorem

{s t u : Subtype p} (h₁ : s ≈ t) (h₂ : t ≈ u) : s ≈ u

Full source

protected theorem trans {s t u : Subtype p} (h₁ : s ≈ t) (h₂ : t ≈ u) : s ≈ u :=
  Setoid.trans h₁ h₂

Transitivity of Inherited Equivalence Relation on Subtypes

Informal description

For any elements $s, t, u$ in the subtype $\{x : \alpha \mid p x\}$ equipped with an inherited equivalence relation $\approx$, if $s \approx t$ and $t \approx u$, then $s \approx u$.

Subtype.equivalence theorem

(p : α → Prop) : Equivalence (@HasEquiv.Equiv (Subtype p) _)

Full source

theorem equivalence (p : α → Prop) : Equivalence (@HasEquiv.Equiv (Subtype p) _) :=
  .mk (Subtype.refl) (@Subtype.symm _ p _) (@Subtype.trans _ p _)

Equivalence Relation Properties on Subtypes

Informal description

For any type $\alpha$ with an equivalence relation $\approx$ and any predicate $p : \alpha \to \mathrm{Prop}$, the inherited equivalence relation on the subtype $\{x : \alpha \mid p x\}$ is an equivalence relation (i.e., it is reflexive, symmetric, and transitive).

Subtype.instSetoid_mathlib instance

(p : α → Prop) : Setoid (Subtype p)

Full source

instance (p : α → Prop) : Setoid (Subtype p) :=
  Setoid.mk (· ≈ ·) (equivalence p)

Setoid Structure on Subtypes

Informal description

For any type $\alpha$ and predicate $p : \alpha \to \mathrm{Prop}$, the subtype $\{x : \alpha \mid p x\}$ has a canonical setoid structure inherited from $\alpha$.

Subtype.coe_prop theorem

{S : Set α} (a : { a // a ∈ S }) : ↑a ∈ S

Full source

@[simp]
theorem coe_prop {S : Set α} (a : { a // a ∈ S }) : ↑a ∈ S :=
  a.prop

Coercion Preserves Subtype Membership Property

Informal description

For any set $S$ of elements of type $\alpha$ and any element $a$ of the subtype $\{a \in \alpha \mid a \in S\}$, the underlying value $a$ (obtained via coercion) belongs to $S$.

Subtype.val_prop theorem

{S : Set α} (a : { a // a ∈ S }) : a.val ∈ S

Full source

theorem val_prop {S : Set α} (a : { a // a ∈ S }) : a.val ∈ S :=
  a.property

Subtype Value Membership Property

Informal description

For any set $S$ of elements of type $\alpha$ and any element $a$ of the subtype $\{a \in \alpha \mid a \in S\}$, the underlying value $a.\mathrm{val}$ belongs to $S$.