mathlib documentation

core.init.coe

@[class]
structure has_lift  :
Sort uSort vSort (max 1 (imax u v))
  • lift : a → b

Can perform a lifting operation ↑a.

Instances
@[class]
structure has_lift_t  :
Sort uSort vSort (max 1 (imax u v))
  • lift : a → b

Auxiliary class that contains the transitive closure of has_lift.

Instances
@[class]
structure has_coe  :
Sort uSort vSort (max 1 (imax u v))
  • coe : a → b

Instances
@[class]
structure has_coe_to_fun  :
Sort uSort (max u (v+1))

Instances
@[class]
structure has_coe_to_sort  :
Sort uType (max u (v+1))

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

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

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

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

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

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

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

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

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

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

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

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

Equations
@[instance]
def coe_option {a : Type u} :

Equations
@[class]
structure has_coe_t_aux  :
Sort uSort vSort (max 1 (imax u v))
  • coe : a → b

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

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

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

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

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

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]
def coe_subtype {a : Sort u} {p : a → Prop} :
has_coe {x // p x} a

Equations
@[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
@[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
@[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
@[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
@[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
@[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
@[instance]
def lift_list {a : Type u} {b : Type v} [has_lift_t a b] :

Equations