mathlib documentation

topology.locally_constant.algebra

Algebraic structure on locally constant functions #

This file puts algebraic structure (add_group, etc) on the type of locally constant functions.

@[instance]
def locally_constant.has_zero {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero Y] :
@[instance]
def locally_constant.has_one {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] :
Equations
@[simp]
theorem locally_constant.one_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] (x : X) :
1 x = 1
@[simp]
theorem locally_constant.zero_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero Y] (x : X) :
0 x = 0
@[instance]
def locally_constant.has_neg {X : Type u_1} {Y : Type u_2} [topological_space X] [has_neg Y] :
@[instance]
def locally_constant.has_inv {X : Type u_1} {Y : Type u_2} [topological_space X] [has_inv Y] :
Equations
@[simp]
theorem locally_constant.inv_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_inv Y] (f : locally_constant X Y) (x : X) :
@[simp]
theorem locally_constant.neg_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_neg Y] (f : locally_constant X Y) (x : X) :
(-f) x = -f x
@[instance]
def locally_constant.has_mul {X : Type u_1} {Y : Type u_2} [topological_space X] [has_mul Y] :
Equations
@[instance]
def locally_constant.has_add {X : Type u_1} {Y : Type u_2} [topological_space X] [has_add Y] :
@[simp]
theorem locally_constant.mul_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_mul Y] (f g : locally_constant X Y) (x : X) :
(f * g) x = (f x) * g x
@[simp]
theorem locally_constant.add_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_add Y] (f g : locally_constant X Y) (x : X) :
(f + g) x = f x + g x
@[instance]
@[instance]
def locally_constant.has_div {X : Type u_1} {Y : Type u_2} [topological_space X] [has_div Y] :
Equations
@[instance]
def locally_constant.has_sub {X : Type u_1} {Y : Type u_2} [topological_space X] [has_sub Y] :
theorem locally_constant.sub_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_sub Y] (f g : locally_constant X Y) (x : X) :
(f - g) x = f x - g x
theorem locally_constant.div_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_div Y] (f g : locally_constant X Y) (x : X) :
(f / g) x = f x / g x
@[instance]
@[instance]
def locally_constant.add_monoid {X : Type u_1} {Y : Type u_2} [topological_space X] [add_monoid Y] :
@[instance]
@[instance]
def locally_constant.add_group {X : Type u_1} {Y : Type u_2} [topological_space X] [add_group Y] :
@[instance]