mathlib docs: core.init.coe

source

@[class]

structure has_lift :

Sort u → Sort v → Sort (max 1 (imax u v))

lift : a → b

Can perform a lifting operation ↑a.

Instances

source

@[class]

structure has_lift_t :

Sort u → Sort v → Sort (max 1 (imax u v))

lift : a → b

Auxiliary class that contains the transitive closure of has_lift.

Instances

source

@[class]

structure has_coe :

Sort u → Sort v → Sort (max 1 (imax u v))

coe : a → b

Instances

source

@[class]

structure has_coe_t :

Sort u → Sort v → Sort (max 1 (imax u v))

coe : a → b

Auxiliary class that contains the transitive closure of has_coe.

Instances

source

@[class]

structure has_coe_to_fun :

Sort u → Sort (max u (v+1))

F : a → Sort ?
coe : Π (x : a), has_coe_to_fun.F x

Instances

source

@[class]

structure has_coe_to_sort :

Sort u → Type (max u (v+1))

S : Sort ?
coe : a → has_coe_to_sort.S a

Instances

coe_sort_trans
coe_sort_bool
set.has_coe_to_sort
category_theory.induced_category.has_coe_to_sort
category_theory.bundled.has_coe_to_sort
submonoid.has_coe_to_sort
add_submonoid.has_coe_to_sort
subgroup.has_coe_to_sort
add_subgroup.has_coe_to_sort
Mon.has_coe_to_sort
AddMon.has_coe_to_sort
CommMon.has_coe_to_sort
AddCommMon.has_coe_to_sort
Group.has_coe_to_sort
AddGroup.has_coe_to_sort
CommGroup.has_coe_to_sort
AddCommGroup.has_coe_to_sort
SemiRing.has_coe_to_sort
Ring.has_coe_to_sort
CommSemiRing.has_coe_to_sort
CommRing.has_coe_to_sort
submodule.has_coe_to_sort
Module.has_coe_to_sort
subsemiring.has_coe_to_sort
Algebra.has_coe_to_sort
Top.has_coe_to_sort
category_theory.Cat.has_coe_to_sort
Meas.has_coe_to_sort
Preorder.has_coe_to_sort
PartialOrder.has_coe_to_sort
LinearOrder.has_coe_to_sort
NonemptyFinLinOrd.has_coe_to_sort
TopCommRing.has_coe_to_sort
UniformSpace.has_coe_to_sort
CpltSepUniformSpace.has_coe_to_sort

source

def lift {a : Sort u} {b : Sort v} [has_lift a b] :

a → b

Equations

lift = has_lift.lift

source

def lift_t {a : Sort u} {b : Sort v} [has_lift_t a b] :

a → b

Equations

lift_t = has_lift_t.lift

source

def coe_b {a : Sort u} {b : Sort v} [has_coe a b] :

a → b

Equations

coe_b = has_coe.coe

source

def coe_t {a : Sort u} {b : Sort v} [has_coe_t a b] :

a → b

Equations

coe_t = has_coe_t.coe

source

def coe_fn_b {a : Sort u} [has_coe_to_fun a] (x : a) :

has_coe_to_fun.F x

Equations

coe_fn_b = has_coe_to_fun.coe

source

def coe {a : Sort u} {b : Sort v} [has_lift_t a b] :

a → b

Equations

coe = lift_t

source

def coe_fn {a : Sort u} [has_coe_to_fun a] (x : a) :

has_coe_to_fun.F x

Equations

coe_fn = has_coe_to_fun.coe

source

def coe_sort {a : Sort u} [has_coe_to_sort a] :

a → has_coe_to_sort.S a

Equations

coe_sort = has_coe_to_sort.coe

source

@[instance]

def lift_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_lift_t b c] [has_lift a b] :

has_lift_t a c

Equations

lift_trans = {lift := λ (x : a), lift_t (lift x)}

source

@[instance]

def lift_base {a : Sort u} {b : Sort v} [has_lift a b] :

has_lift_t a b

Equations

lift_base = {lift := lift _inst_1}

source

@[instance]

def coe_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe_t b c] [has_coe a b] :

has_coe_t a c

Equations

coe_trans = {coe := λ (x : a), coe_t (coe_b x)}

source

@[instance]

def coe_base {a : Sort u} {b : Sort v} [has_coe a b] :

has_coe_t a b

Equations

coe_base = {coe := coe_b _inst_1}

source

@[instance]

def coe_option {a : Type u} :

has_coe_t a (option a)

Equations

coe_option = {coe := λ (x : a), option.some x}

source

@[class]

structure has_coe_t_aux :

Sort u → Sort v → Sort (max 1 (imax u v))

coe : a → b

Instances

source

@[instance]

def coe_trans_aux {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe_t_aux b c] [has_coe a b] :

has_coe_t_aux a c

Equations

coe_trans_aux = {coe := λ (x : a), has_coe_t_aux.coe (coe_b x)}

source

@[instance]

def coe_base_aux {a : Sort u} {b : Sort v} [has_coe a b] :

has_coe_t_aux a b

Equations

coe_base_aux = {coe := coe_b _inst_1}

source

@[instance]

def coe_fn_trans {a : Sort u₁} {b : Sort u₂} [has_coe_to_fun b] [has_coe_t_aux a b] :

has_coe_to_fun a

Equations

coe_fn_trans = {F := λ (x : a), has_coe_to_fun.F (has_coe_t_aux.coe x), coe := λ (x : a), ⇑(has_coe_t_aux.coe x)}

source

@[instance]

def coe_sort_trans {a : Sort u₁} {b : Sort u₂} [has_coe_to_sort b] [has_coe_t_aux a b] :

has_coe_to_sort a

Equations

coe_sort_trans = {S := has_coe_to_sort.S b _inst_1, coe := λ (x : a), ↥(has_coe_t_aux.coe x)}

source

@[instance]

def coe_to_lift {a : Sort u} {b : Sort v} [has_coe_t a b] :

has_lift_t a b

Equations

coe_to_lift = {lift := coe_t _inst_1}

source

@[instance]

def coe_bool_to_Prop :

has_coe bool Prop

Equations

coe_bool_to_Prop = {coe := λ (y : bool), y = bool.tt}

source

@[instance]

def coe_sort_bool :

has_coe_to_sort bool

Equations

coe_sort_bool = {S := Prop, coe := λ (y : bool), y = bool.tt}

source

@[instance]

def coe_decidable_eq (x : bool) :

decidable ↑x

Equations

coe_decidable_eq x = show decidable (x = bool.tt), from bool.decidable_eq x bool.tt

source

@[instance]

def coe_subtype {a : Sort u} {p : a → Prop} :

has_coe {x // p x} a

Equations

coe_subtype = {coe := subtype.val (λ (x : a), p x)}

source

@[instance]

def lift_fn {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [has_lift a₂ a₁] [has_lift_t b₁ b₂] :

has_lift (a₁ → b₁) (a₂ → b₂)

Equations

lift_fn = {lift := λ (f : a₁ → b₁) (x : a₂), ↑(f ↑x)}

source

@[instance]

def lift_fn_range {a : Sort ua} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [has_lift_t b₁ b₂] :

has_lift (a → b₁) (a → b₂)

Equations

lift_fn_range = {lift := λ (f : a → b₁) (x : a), ↑(f x)}

source

@[instance]

def lift_fn_dom {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b : Sort ub} [has_lift a₂ a₁] :

has_lift (a₁ → b) (a₂ → b)

Equations

lift_fn_dom = {lift := λ (f : a₁ → b) (x : a₂), f ↑x}

source

@[instance]

def lift_pair {a₁ : Type ua₁} {a₂ : Type ub₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t a₁ a₂] [has_lift_t b₁ b₂] :

has_lift (a₁ × b₁) (a₂ × b₂)

Equations

lift_pair = {lift := λ (p : a₁ × b₁), p.cases_on (λ (x : a₁) (y : b₁), (↑x, ↑y))}

source

@[instance]

def lift_pair₁ {a₁ : Type ua₁} {a₂ : Type ua₂} {b : Type ub} [has_lift_t a₁ a₂] :

has_lift (a₁ × b) (a₂ × b)

Equations

lift_pair₁ = {lift := λ (p : a₁ × b), p.cases_on (λ (x : a₁) (y : b), (↑x, y))}

source

@[instance]

def lift_pair₂ {a : Type ua} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t b₁ b₂] :

has_lift (a × b₁) (a × b₂)

Equations

lift_pair₂ = {lift := λ (p : a × b₁), p.cases_on (λ (x : a) (y : b₁), (x, ↑y))}

source

@[instance]

def lift_list {a : Type u} {b : Type v} [has_lift_t a b] :

has_lift (list a) (list b)

Equations

lift_list = {lift := λ (l : list a), list.map coe l}

mathlib documentation

core.init.coe

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​coe

General documentation

Additional documentation

Library

core.init.coe