mathlib docs: data.subtype

theorem subtype.prop {α : Sort u_1} {p : α → Prop} (x : subtype p) :

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.

source

@[simp]

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

x.val = ↑x

source

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

source

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.

source

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

source

@[ext]

theorem subtype.ext {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :

↑a1 = ↑a2 → a1 = a2

source

theorem subtype.ext_iff {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :

a1 = a2 ↔ ↑a1 = ↑a2

source

theorem subtype.ext_val {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :

a1.val = a2.val → a1 = a2

source

theorem subtype.ext_iff_val {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :

a1 = a2 ↔ a1.val = a2.val

source

@[simp]

theorem subtype.coe_eta {α : Sort u_1} {p : α → Prop} (a : {a // p a}) (h : p ↑a) :

⟨↑a, h⟩ = a

source

@[simp]

theorem subtype.coe_mk {α : Sort u_1} {p : α → Prop} (a : α) (h : p a) :

↑⟨a, h⟩ = a

source

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

source

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

function.injective coe

source

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

function.injective subtype.val

source

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

β x.val

Restrict a (dependent) function to a subtype

Equations

subtype.restrict f p x = f ↑x

source

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

subtype.restrict f p x = f x.val

source

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

subtype.restrict f p = f ∘ coe

source

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

function.injective f → function.injective (subtype.restrict f p)

source

def subtype.coind {α : Sort u_1} {β : Sort u_2} (f : α → β) {p : β → Prop} :

(∀ (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, _⟩

source

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

function.injective f → function.injective (subtype.coind f h)

source

def subtype.map {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) :

(∀ (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, _⟩

source

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

source