mathlib documentation

core / init.coe

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

Can perform a lifting operation ↑a.

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

Auxiliary class that contains the transitive closure of has_lift.

Instances
@[class]
structure has_coe (a : Sort u) (b : Sort v) :
Sort (max 1 (imax u v))
  • coe : a → b
Instances
@[class]
structure has_coe_to_fun (a : Sort u) :
Sort (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 (a : Sort u) (b : Sort v) :
Sort (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