Locally constant functions #
This file sets up the theory of locally constant function from a topological space to a type.
Main definitions and constructions #
IsLocallyConstant f
: a mapf : X → Y
whereX
is a topological space is locally constant if every set inY
has an open preimage.LocallyConstant X Y
: the type of locally constant maps fromX
toY
LocallyConstant.map
: push-forward of locally constant mapsLocallyConstant.comap
: pull-back of locally constant maps
A function between topological spaces is locally constant if the preimage of any set is open.
Instances For
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
.
- toFun : X → Y
The underlying function.
- isLocallyConstant : IsLocallyConstant s.toFun
The map is locally constant.
A (bundled) locally constant function from a topological space X
to a type Y
.
Instances For
See Note [custom simps projections].
Instances For
We can turn a locally-constant function into a bundled ContinuousMap
.
Instances For
As a shorthand, LocallyConstant.toContinuousMap
is available as a coercion
The constant locally constant function on X
with value y : Y
.
Instances For
The locally constant function to Fin 2
associated to a clopen set.
Instances For
Push forward of locally constant maps under any map, by post-composition.
Instances For
Given a locally constant function to α → β
, construct a family of locally constant
functions with values in β indexed by α.
Instances For
If α is finite, this constructs a locally constant function to α → β
given a
family of locally constant functions with values in β indexed by α.
Instances For
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 LocallyConstant.coe_comap
.
TODO: take f : C(X, Y)
as an argument? Or we actually use it for discontinuous f
?
Instances For
If a locally constant function factors through an injection, then it factors through a locally constant function.
Instances For
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.
Instances For
Given a clopen set U
and a locally constant function f
, LocallyConstant.mulIndicator
returns the locally constant function that is f
on U
and 1
otherwise.
Instances For
The equivalence between LocallyConstant X Z
and LocallyConstant Y Z
given a
homeomorphism X ≃ₜ Y
Instances For
Given two closed sets covering a topological space, and locally constant maps on these two sets, then if these two locally constant maps agree on the intersection, we get a piecewise defined locally constant map on the whole space.