Locally constant functions #
This file sets up the theory of locally constant function from a topological space to a type.
Main definitions and constructions #
is_locally_constant f
: a mapf : X → Y
whereX
is a topological space is locally constant if every set inY
has an open preimage.locally_constant X Y
: the type of locally constant maps fromX
toY
locally_constant.map
: push-forward of locally constant mapslocally_constant.comap
: pull-back of locally constant maps
A function between topological spaces is locally constant if the preimage of any set is open.
Equations
- is_locally_constant f = ∀ (s : set Y), is_open (f ⁻¹' s)
A locally constant function is constant on any preconnected set.
If a composition of a function f
followed by an injection g
is locally
constant, then the locally constant property descends to f
.
- to_fun : X → Y
- is_locally_constant : is_locally_constant self.to_fun
A (bundled) locally constant function from a topological space X
to a type Y
.
Instances for locally_constant
- locally_constant.has_sizeof_inst
- locally_constant.inhabited
- locally_constant.has_coe_to_fun
- locally_constant.continuous_map.has_coe
- locally_constant.has_one
- locally_constant.has_zero
- locally_constant.has_inv
- locally_constant.has_neg
- locally_constant.has_mul
- locally_constant.has_add
- locally_constant.mul_one_class
- locally_constant.add_zero_class
- locally_constant.mul_zero_class
- locally_constant.mul_zero_one_class
- locally_constant.has_div
- locally_constant.has_sub
- locally_constant.semigroup
- locally_constant.add_semigroup
- locally_constant.semigroup_with_zero
- locally_constant.comm_semigroup
- locally_constant.add_comm_semigroup
- locally_constant.monoid
- locally_constant.add_monoid
- locally_constant.add_monoid_with_one
- locally_constant.comm_monoid
- locally_constant.add_comm_monoid
- locally_constant.group
- locally_constant.add_group
- locally_constant.comm_group
- locally_constant.add_comm_group
- locally_constant.distrib
- locally_constant.non_unital_non_assoc_semiring
- locally_constant.non_unital_semiring
- locally_constant.non_assoc_semiring
- locally_constant.semiring
- locally_constant.non_unital_comm_semiring
- locally_constant.comm_semiring
- locally_constant.non_unital_non_assoc_ring
- locally_constant.non_unital_ring
- locally_constant.non_assoc_ring
- locally_constant.ring
- locally_constant.non_unital_comm_ring
- locally_constant.comm_ring
- locally_constant.has_smul
- locally_constant.mul_action
- locally_constant.distrib_mul_action
- locally_constant.module
- locally_constant.algebra
Equations
Equations
- locally_constant.has_coe_to_fun = {coe := locally_constant.to_fun _inst_1}
We can turn a locally-constant function into a bundled continuous_map
.
Equations
- f.to_continuous_map = {to_fun := ⇑f, continuous_to_fun := _}
As a shorthand, locally_constant.to_continuous_map
is available as a coercion
Equations
The constant locally constant function on X
with value y : Y
.
Equations
- locally_constant.const X y = {to_fun := function.const X y, is_locally_constant := _}
The locally constant function to fin 2
associated to a clopen set.
Equations
- locally_constant.of_clopen hU = {to_fun := λ (x : X), ite (x ∈ U) 0 1, is_locally_constant := _}
Push forward of locally constant maps under any map, by post-composition.
Equations
- locally_constant.map f = λ (g : locally_constant X Y), {to_fun := f ∘ ⇑g, is_locally_constant := _}
Given a locally constant function to α → β
, construct a family of locally constant
functions with values in β indexed by α.
Equations
- f.flip a = locally_constant.map (λ (f : α → β), f a) f
If α is finite, this constructs a locally constant function to α → β
given a
family of locally constant functions with values in β indexed by α.
Equations
- locally_constant.unflip f = {to_fun := λ (x : X) (a : α), ⇑(f a) x, is_locally_constant := _}
Pull back of locally constant maps under any map, by pre-composition.
This definition only makes sense if f
is continuous,
in which case it sends locally constant functions to their precomposition with f
.
See also locally_constant.coe_comap
.
Equations
- locally_constant.comap f = dite (continuous f) (λ (hf : continuous f) (g : locally_constant Y Z), {to_fun := ⇑g ∘ f, is_locally_constant := _}) (λ (hf : ¬continuous f), dite (nonempty X) (λ (H : nonempty X) (g : locally_constant Y Z), locally_constant.const X (⇑g (f (classical.arbitrary X)))) (λ (H : ¬nonempty X) (g : locally_constant Y Z), {to_fun := λ (x : X), _.elim, is_locally_constant := _}))
If a locally constant function factors through an injection, then it factors through a locally constant function.
Equations
- locally_constant.desc f h cond inj = {to_fun := f, is_locally_constant := _}
Given a clopen set U
and a locally constant function f
,
locally_constant.indicator
returns the locally constant function that is f
on U
and 0
otherwise.
Given a clopen set U
and a locally constant function f
, locally_constant.mul_indicator
returns the locally constant function that is f
on U
and 1
otherwise.
Equations
- f.mul_indicator hU = {to_fun := U.mul_indicator ⇑f, is_locally_constant := _}