# Documentation

Mathlib.Topology.LocallyConstant.Basic

# 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 map f : X → Y where X is a topological space is locally constant if every set in Y has an open preimage.
• LocallyConstant X Y : the type of locally constant maps from X to Y
• LocallyConstant.map : push-forward of locally constant maps
• LocallyConstant.comap : pull-back of locally constant maps
def IsLocallyConstant {X : Type u_1} {Y : Type u_2} [] (f : XY) :

A function between topological spaces is locally constant if the preimage of any set is open.

Instances For
theorem IsLocallyConstant.tfae {X : Type u_1} {Y : Type u_2} [] (f : XY) :
List.TFAE [, ∀ (x : X), ∀ᶠ (x' : X) in nhds x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x}, ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), U, x U ∀ (x' : X), x' Uf x' = f x]
theorem IsLocallyConstant.of_discrete {X : Type u_1} {Y : Type u_2} [] [] (f : XY) :
theorem IsLocallyConstant.isOpen_fiber {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (y : Y) :
IsOpen {x | f x = y}
theorem IsLocallyConstant.isClosed_fiber {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (y : Y) :
IsClosed {x | f x = y}
theorem IsLocallyConstant.isClopen_fiber {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (y : Y) :
IsClopen {x | f x = y}
theorem IsLocallyConstant.iff_exists_open {X : Type u_1} {Y : Type u_2} [] (f : XY) :
∀ (x : X), U, x U ∀ (x' : X), x' Uf x' = f x
theorem IsLocallyConstant.iff_eventually_eq {X : Type u_1} {Y : Type u_2} [] (f : XY) :
∀ (x : X), ∀ᶠ (y : X) in nhds x, f y = f x
theorem IsLocallyConstant.exists_open {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (x : X) :
U, x U ∀ (x' : X), x' Uf x' = f x
theorem IsLocallyConstant.eventually_eq {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (x : X) :
∀ᶠ (y : X) in nhds x, f y = f x
theorem IsLocallyConstant.iff_isOpen_fiber_apply {X : Type u_1} {Y : Type u_2} [] {f : XY} :
∀ (x : X), IsOpen (f ⁻¹' {f x})
theorem IsLocallyConstant.iff_isOpen_fiber {X : Type u_1} {Y : Type u_2} [] {f : XY} :
∀ (y : Y), IsOpen (f ⁻¹' {y})
theorem IsLocallyConstant.continuous {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsLocallyConstant.iff_continuous {X : Type u_1} {Y : Type u_2} [] :
∀ {x : } [inst : ] (f : XY),
theorem IsLocallyConstant.of_constant {X : Type u_1} {Y : Type u_2} [] (f : XY) (h : ∀ (x y : X), f x = f y) :
theorem IsLocallyConstant.const {X : Type u_1} {Y : Type u_2} [] (y : Y) :
theorem IsLocallyConstant.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] {f : XY} (hf : ) (g : YZ) :
theorem IsLocallyConstant.prod_mk {X : Type u_1} {Y : Type u_2} [] {Y' : Type u_5} {f : XY} {f' : XY'} (hf : ) (hf' : ) :
IsLocallyConstant fun x => (f x, f' x)
theorem IsLocallyConstant.comp₂ {X : Type u_1} [] {Y₁ : Type u_5} {Y₂ : Type u_6} {Z : Type u_7} {f : XY₁} {g : XY₂} (hf : ) (hg : ) (h : Y₁Y₂Z) :
IsLocallyConstant fun x => h (f x) (g x)
theorem IsLocallyConstant.comp_continuous {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] {g : YZ} {f : XY} (hg : ) (hf : ) :
theorem IsLocallyConstant.apply_eq_of_isPreconnected {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) {s : Set X} (hs : ) {x : X} {y : X} (hx : x s) (hy : y s) :
f x = f y

A locally constant function is constant on any preconnected set.

theorem IsLocallyConstant.apply_eq_of_preconnectedSpace {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (x : X) (y : X) :
f x = f y
theorem IsLocallyConstant.eq_const {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (x : X) :
f = Function.const X (f x)
theorem IsLocallyConstant.exists_eq_const {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
y, f =
theorem IsLocallyConstant.iff_is_const {X : Type u_1} {Y : Type u_2} [] {f : XY} :
∀ (x y : X), f x = f y
theorem IsLocallyConstant.range_finite {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsLocallyConstant.zero {X : Type u_1} {Y : Type u_2} [] [Zero Y] :
theorem IsLocallyConstant.one {X : Type u_1} {Y : Type u_2} [] [One Y] :
theorem IsLocallyConstant.neg {X : Type u_1} {Y : Type u_2} [] [Neg Y] ⦃f : XY (hf : ) :
theorem IsLocallyConstant.inv {X : Type u_1} {Y : Type u_2} [] [Inv Y] ⦃f : XY (hf : ) :
theorem IsLocallyConstant.add {X : Type u_1} {Y : Type u_2} [] [Add Y] ⦃f : XY ⦃g : XY (hf : ) (hg : ) :
theorem IsLocallyConstant.mul {X : Type u_1} {Y : Type u_2} [] [Mul Y] ⦃f : XY ⦃g : XY (hf : ) (hg : ) :
theorem IsLocallyConstant.sub {X : Type u_1} {Y : Type u_2} [] [Sub Y] ⦃f : XY ⦃g : XY (hf : ) (hg : ) :
theorem IsLocallyConstant.div {X : Type u_1} {Y : Type u_2} [] [Div Y] ⦃f : XY ⦃g : XY (hf : ) (hg : ) :
theorem IsLocallyConstant.desc {X : Type u_1} [] {α : Type u_5} {β : Type u_6} (f : Xα) (g : αβ) (h : IsLocallyConstant (g f)) (inj : ) :

If a composition of a function f followed by an injection g is locally constant, then the locally constant property descends to f.

theorem IsLocallyConstant.of_constant_on_connected_components {X : Type u_1} {Y : Type u_2} [] {f : XY} (h : ∀ (x y : X), f y = f x) :
theorem IsLocallyConstant.of_constant_on_connected_clopens {X : Type u_1} {Y : Type u_2} [] {f : XY} (h : ∀ (U : Set X), ∀ (x : X), x U∀ (y : X), y Uf y = f x) :
theorem IsLocallyConstant.of_constant_on_preconnected_clopens {X : Type u_1} {Y : Type u_2} [] {f : XY} (h : ∀ (U : Set X), ∀ (x : X), x U∀ (y : X), y Uf y = f x) :
structure LocallyConstant (X : Type u_5) (Y : Type u_6) [] :
Type (max u_5 u_6)
• toFun : XY

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
instance LocallyConstant.instFunLikeLocallyConstant {X : Type u_1} {Y : Type u_2} [] :
FunLike () X fun x => Y
def LocallyConstant.Simps.apply {X : Type u_1} {Y : Type u_2} [] (f : ) :
XY

See Note [custom simps projections].

Instances For
@[simp]
theorem LocallyConstant.toFun_eq_coe {X : Type u_1} {Y : Type u_2} [] (f : ) :
f.toFun = f
@[simp]
theorem LocallyConstant.coe_mk {X : Type u_1} {Y : Type u_2} [] (f : XY) (h : ) :
{ toFun := f, isLocallyConstant := h } = f
theorem LocallyConstant.congr_fun {X : Type u_1} {Y : Type u_2} [] {f : } {g : } (h : f = g) (x : X) :
f x = g x
theorem LocallyConstant.congr_arg {X : Type u_1} {Y : Type u_2} [] (f : ) {x : X} {y : X} (h : x = y) :
f x = f y
theorem LocallyConstant.coe_injective {X : Type u_1} {Y : Type u_2} [] :
Function.Injective FunLike.coe
theorem LocallyConstant.coe_inj {X : Type u_1} {Y : Type u_2} [] {f : } {g : } :
f = g f = g
theorem LocallyConstant.ext {X : Type u_1} {Y : Type u_2} [] ⦃f : ⦃g : (h : ∀ (x : X), f x = g x) :
f = g
theorem LocallyConstant.ext_iff {X : Type u_1} {Y : Type u_2} [] {f : } {g : } :
f = g ∀ (x : X), f x = g x
theorem LocallyConstant.continuous {X : Type u_1} {Y : Type u_2} [] [] (f : ) :
def LocallyConstant.toContinuousMap {X : Type u_1} {Y : Type u_2} [] [] (f : ) :
C(X, Y)

We can turn a locally-constant function into a bundled ContinuousMap.

Instances For
instance LocallyConstant.instCoeLocallyConstantContinuousMap {X : Type u_1} {Y : Type u_2} [] [] :
Coe () C(X, Y)

As a shorthand, LocallyConstant.toContinuousMap is available as a coercion

@[simp]
theorem LocallyConstant.coe_continuousMap {X : Type u_1} {Y : Type u_2} [] [] (f : ) :
f = f
theorem LocallyConstant.toContinuousMap_injective {X : Type u_1} {Y : Type u_2} [] [] :
Function.Injective LocallyConstant.toContinuousMap
def LocallyConstant.const (X : Type u_5) {Y : Type u_6} [] (y : Y) :

The constant locally constant function on X with value y : Y.

Instances For
@[simp]
theorem LocallyConstant.coe_const {X : Type u_1} {Y : Type u_2} [] (y : Y) :
↑() =
def LocallyConstant.ofClopen {X : Type u_5} [] {U : Set X} [(x : X) → Decidable (x U)] (hU : ) :

The locally constant function to Fin 2 associated to a clopen set.

Instances For
@[simp]
theorem LocallyConstant.ofClopen_fiber_zero {X : Type u_5} [] {U : Set X} [(x : X) → Decidable (x U)] (hU : ) :
↑() ⁻¹' {0} = U
@[simp]
theorem LocallyConstant.ofClopen_fiber_one {X : Type u_5} [] {U : Set X} [(x : X) → Decidable (x U)] (hU : ) :
↑() ⁻¹' {1} = U
theorem LocallyConstant.locallyConstant_eq_of_fiber_zero_eq {X : Type u_5} [] (f : LocallyConstant X (Fin 2)) (g : LocallyConstant X (Fin 2)) (h : f ⁻¹' {0} = g ⁻¹' {0}) :
f = g
theorem LocallyConstant.range_finite {X : Type u_1} {Y : Type u_2} [] [] (f : ) :
theorem LocallyConstant.apply_eq_of_isPreconnected {X : Type u_1} {Y : Type u_2} [] (f : ) {s : Set X} (hs : ) {x : X} {y : X} (hx : x s) (hy : y s) :
f x = f y
theorem LocallyConstant.apply_eq_of_preconnectedSpace {X : Type u_1} {Y : Type u_2} [] (f : ) (x : X) (y : X) :
f x = f y
theorem LocallyConstant.eq_const {X : Type u_1} {Y : Type u_2} [] (f : ) (x : X) :
theorem LocallyConstant.exists_eq_const {X : Type u_1} {Y : Type u_2} [] [] (f : ) :
y,
def LocallyConstant.map {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] (f : YZ) (g : ) :

Push forward of locally constant maps under any map, by post-composition.

Instances For
@[simp]
theorem LocallyConstant.map_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] (f : YZ) (g : ) :
↑() = f g
@[simp]
theorem LocallyConstant.map_id {X : Type u_1} {Y : Type u_2} [] :
= id
@[simp]
theorem LocallyConstant.map_comp {X : Type u_1} [] {Y₁ : Type u_5} {Y₂ : Type u_6} {Y₃ : Type u_7} (g : Y₂Y₃) (f : Y₁Y₂) :
def LocallyConstant.flip {X : Type u_5} {α : Type u_6} {β : Type u_7} [] (f : LocallyConstant X (αβ)) (a : α) :

Given a locally constant function to α → β, construct a family of locally constant functions with values in β indexed by α.

Instances For
def LocallyConstant.unflip {X : Type u_5} {α : Type u_6} {β : Type u_7} [] [] (f : α) :
LocallyConstant X (αβ)

If α is finite, this constructs a locally constant function to α → β given a family of locally constant functions with values in β indexed by α.

Instances For
@[simp]
theorem LocallyConstant.unflip_flip {X : Type u_5} {α : Type u_6} {β : Type u_7} [] [] (f : LocallyConstant X (αβ)) :
@[simp]
theorem LocallyConstant.flip_unflip {X : Type u_5} {α : Type u_6} {β : Type u_7} [] [] (f : α) :
noncomputable def LocallyConstant.comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : XY) :

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
@[simp]
theorem LocallyConstant.coe_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : XY) (g : ) (hf : ) :
↑() = g f
theorem LocallyConstant.coe_comap_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : XY) (g : ) (hf : ) (x : X) :
↑() x = g (f x)
@[simp]
theorem LocallyConstant.comap_id {X : Type u_1} {Z : Type u_3} [] :
theorem LocallyConstant.comap_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {α : Type u_4} [] [] [] (f : XY) (g : YZ) (hf : ) (hg : ) :
theorem LocallyConstant.comap_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {α : Type u_4} [] [] [] (f : XY) (g : YZ) (hf : ) (hg : ) (x : ) :
theorem LocallyConstant.comap_const {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : XY) (y : Y) (h : ∀ (x : X), f x = y) :
= fun g => LocallyConstant.const X (g y)
theorem LocallyConstant.comap_injective {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : XY) (hf : ) (hfs : ) :
def LocallyConstant.desc {X : Type u_5} {α : Type u_6} {β : Type u_7} [] {g : αβ} (f : Xα) (h : ) (cond : g f = h) (inj : ) :

If a locally constant function factors through an injection, then it factors through a locally constant function.

Instances For
@[simp]
theorem LocallyConstant.coe_desc {X : Type u_5} {α : Type u_6} {β : Type u_7} [] (f : Xα) (g : αβ) (h : ) (cond : g f = h) (inj : ) :
↑(LocallyConstant.desc f h cond inj) = f
theorem LocallyConstant.indicator.proof_1 {X : Type u_2} [] {R : Type u_1} [Zero R] {U : Set X} (f : ) (hU : ) (s : Set R) :
noncomputable def LocallyConstant.indicator {X : Type u_1} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) (hU : ) :

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
@[simp]
theorem LocallyConstant.mulIndicator_apply {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) (hU : ) (x : X) :
↑() x = Set.mulIndicator U (f) x
@[simp]
theorem LocallyConstant.indicator_apply {X : Type u_1} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) (hU : ) (x : X) :
↑() x = Set.indicator U (f) x
noncomputable def LocallyConstant.mulIndicator {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) (hU : ) :

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
theorem LocallyConstant.indicator_apply_eq_if {X : Type u_1} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) (a : X) (hU : ) :
↑() a = if a U then f a else 0
theorem LocallyConstant.mulIndicator_apply_eq_if {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) (a : X) (hU : ) :
↑() a = if a U then f a else 1
theorem LocallyConstant.indicator_of_mem {X : Type u_1} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) {a : X} (hU : ) (h : a U) :
↑() a = f a
theorem LocallyConstant.mulIndicator_of_mem {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) {a : X} (hU : ) (h : a U) :
↑() a = f a
theorem LocallyConstant.indicator_of_not_mem {X : Type u_1} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) {a : X} (hU : ) (h : ¬a U) :
↑() a = 0
theorem LocallyConstant.mulIndicator_of_not_mem {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) {a : X} (hU : ) (h : ¬a U) :
↑() a = 1
@[simp]
theorem LocallyConstant.congrLeft_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (e : X ≃ₜ Y) :
∀ (a : ), =
@[simp]
theorem LocallyConstant.congrLeft_symm_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (e : X ≃ₜ Y) :
∀ (a : ), ().symm a =
noncomputable def LocallyConstant.congrLeft {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (e : X ≃ₜ Y) :

The equivalence between LocallyConstant X Z and LocallyConstant Y Z given a homeomorphism X ≃ₜ Y

Instances For
def LocallyConstant.piecewise {X : Type u_1} {Z : Type u_3} [] {C₁ : Set X} {C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂) (h : C₁ C₂ = Set.univ) (f : LocallyConstant (C₁) Z) (g : LocallyConstant (C₂) Z) (hfg : ∀ (x : X) (hx : x C₁ C₂), LocallyConstant.toFun f { val := x, property := (_ : x C₁) } = LocallyConstant.toFun g { val := x, property := (_ : x C₂) }) [(j : X) → Decidable (j C₁)] :

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.

Instances For