mathlib documentation

data.subtype

def subtype.simps.val {α : Sort u_1} {p : α → Prop} :
subtype p → α

See Note [custom simps projection]

Equations
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} :
x.val = x

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

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.

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

@[ext]
theorem subtype.ext {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :
a1 = a2a1 = a2

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

theorem subtype.ext_val {α : Sort u_1} {p : α → Prop} {a1 a2 : {x // p x}} :
a1.val = a2.vala1 = 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_injective {α : Sort u_1} {p : α → Prop} :

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

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
theorem subtype.restrict_apply {α : Sort u_1} {β : α → Type u_2} (f : Π (x : α), β x) (p : α → Prop) (x : subtype p) :

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

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

@[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} :
(∀ (a : α), p (f a))α → subtype p

Defining a map into a subtype, this can be seen as an "coinduction principle" of subtype

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

@[simp]
theorem subtype.map_coe {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p aq (f a)) (ᾰ : subtype p) :
(subtype.map f h ᾰ) = f

def subtype.map {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) :
(∀ (a : α), p aq (f a))subtype psubtype q

Restriction of a function to a function on subtypes.

Equations
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) _ x

theorem subtype.map_id {α : Sort u_1} {p : α → Prop} {h : ∀ (a : α), p ap (id a)} :

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

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

Equations
theorem subtype.equiv_iff {α : Sort u_1} [has_equiv α] {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} :
s tt s

theorem subtype.trans {α : Sort u_1} {p : α → Prop} [setoid α] {s t u : subtype p} :
s tt us u

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

@[instance]
def subtype.setoid {α : 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.val S