# mathlib3documentation

topology.locally_constant.basic

# Locally constant functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Equations
@[protected]
theorem is_locally_constant.tfae {X : Type u_1} {Y : Type u_2} (f : X Y) :
[, (x : X), ∀ᶠ (x' : X) in nhds x, f x' = f x, (x : X), is_open {x' : X | f x' = f x}, (y : Y), is_open (f ⁻¹' {y}), (x : X), (U : set X) (hU : is_open U) (hx : x U), (x' : X), x' U f x' = f x].tfae
theorem is_locally_constant.of_discrete {X : Type u_1} {Y : Type u_2} (f : X Y) :
theorem is_locally_constant.is_open_fiber {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) (y : Y) :
is_open {x : X | f x = y}
theorem is_locally_constant.is_closed_fiber {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) (y : Y) :
is_closed {x : X | f x = y}
theorem is_locally_constant.is_clopen_fiber {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) (y : Y) :
is_clopen {x : X | f x = y}
theorem is_locally_constant.iff_exists_open {X : Type u_1} {Y : Type u_2} (f : X Y) :
(x : X), (U : set X) (hU : is_open U) (hx : x U), (x' : X), x' U f x' = f x
theorem is_locally_constant.iff_eventually_eq {X : Type u_1} {Y : Type u_2} (f : X Y) :
(x : X), ∀ᶠ (y : X) in nhds x, f y = f x
theorem is_locally_constant.exists_open {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) (x : X) :
(U : set X) (hU : is_open U) (hx : x U), (x' : X), x' U f x' = f x
@[protected]
theorem is_locally_constant.eventually_eq {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) (x : X) :
∀ᶠ (y : X) in nhds x, f y = f x
@[protected]
theorem is_locally_constant.continuous {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) :
theorem is_locally_constant.iff_continuous {X : Type u_1} {Y : Type u_2} {_x : topological_space Y} (f : X Y) :
theorem is_locally_constant.of_constant {X : Type u_1} {Y : Type u_2} (f : X Y) (h : (x y : X), f x = f y) :
theorem is_locally_constant.const {X : Type u_1} {Y : Type u_2} (y : Y) :
theorem is_locally_constant.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X Y} (hf : is_locally_constant f) (g : Y Z) :
theorem is_locally_constant.prod_mk {X : Type u_1} {Y : Type u_2} {Y' : Type u_3} {f : X Y} {f' : X Y'} (hf : is_locally_constant f) (hf' : is_locally_constant f') :
is_locally_constant (λ (x : X), (f x, f' x))
theorem is_locally_constant.comp₂ {X : Type u_1} {Y₁ : Type u_2} {Y₂ : Type u_3} {Z : Type u_4} {f : X Y₁} {g : X Y₂} (hf : is_locally_constant f) (hg : is_locally_constant g) (h : Y₁ Y₂ Z) :
is_locally_constant (λ (x : X), h (f x) (g x))
theorem is_locally_constant.comp_continuous {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : Y Z} {f : X Y} (hg : is_locally_constant g) (hf : continuous f) :
theorem is_locally_constant.apply_eq_of_is_preconnected {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) {s : set X} (hs : is_preconnected s) {x y : X} (hx : x s) (hy : y s) :
f x = f y

A locally constant function is constant on any preconnected set.

theorem is_locally_constant.apply_eq_of_preconnected_space {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) (x y : X) :
f x = f y
theorem is_locally_constant.eq_const {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) (x : X) :
f = (f x)
theorem is_locally_constant.exists_eq_const {X : Type u_1} {Y : Type u_2} [nonempty Y] {f : X Y} (hf : is_locally_constant f) :
(y : Y), f =
theorem is_locally_constant.iff_is_const {X : Type u_1} {Y : Type u_2} {f : X Y} :
(x y : X), f x = f y
theorem is_locally_constant.range_finite {X : Type u_1} {Y : Type u_2} {f : X Y} (hf : is_locally_constant f) :
theorem is_locally_constant.one {X : Type u_1} {Y : Type u_2} [has_one Y] :
theorem is_locally_constant.zero {X : Type u_1} {Y : Type u_2} [has_zero Y] :
theorem is_locally_constant.neg {X : Type u_1} {Y : Type u_2} [has_neg Y] ⦃f : X Y⦄ (hf : is_locally_constant f) :
theorem is_locally_constant.inv {X : Type u_1} {Y : Type u_2} [has_inv Y] ⦃f : X Y⦄ (hf : is_locally_constant f) :
theorem is_locally_constant.add {X : Type u_1} {Y : Type u_2} [has_add Y] ⦃f g : X Y⦄ (hf : is_locally_constant f) (hg : is_locally_constant g) :
theorem is_locally_constant.mul {X : Type u_1} {Y : Type u_2} [has_mul Y] ⦃f g : X Y⦄ (hf : is_locally_constant f) (hg : is_locally_constant g) :
theorem is_locally_constant.div {X : Type u_1} {Y : Type u_2} [has_div Y] ⦃f g : X Y⦄ (hf : is_locally_constant f) (hg : is_locally_constant g) :
theorem is_locally_constant.sub {X : Type u_1} {Y : Type u_2} [has_sub Y] ⦃f g : X Y⦄ (hf : is_locally_constant f) (hg : is_locally_constant g) :
theorem is_locally_constant.desc {X : Type u_1} {α : Type u_2} {β : Type u_3} (f : X α) (g : α β) (h : is_locally_constant (g f)) (inj : function.injective g) :

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

theorem is_locally_constant.of_constant_on_connected_components {X : Type u_1} {Y : Type u_2} {f : X Y} (h : (x y : X), f y = f x) :
theorem is_locally_constant.of_constant_on_preconnected_clopens {X : Type u_1} {Y : Type u_2} {f : X Y} (h : (U : set X), (x : X), x U (y : X), y U f y = f x) :
structure locally_constant (X : Type u_5) (Y : Type u_6)  :
Type (max u_5 u_6)
• to_fun : X Y
• is_locally_constant :

A (bundled) locally constant function from a topological space X to a type Y.

Instances for locally_constant
@[protected, instance]
def locally_constant.inhabited {X : Type u_1} {Y : Type u_2} [inhabited Y] :
Equations
@[protected, instance]
def locally_constant.has_coe_to_fun {X : Type u_1} {Y : Type u_2}  :
(λ (_x : Y), X Y)
Equations
@[simp]
theorem locally_constant.to_fun_eq_coe {X : Type u_1} {Y : Type u_2} (f : Y) :
@[simp]
theorem locally_constant.coe_mk {X : Type u_1} {Y : Type u_2} (f : X Y) (h : is_locally_constant f) :
theorem locally_constant.congr_fun {X : Type u_1} {Y : Type u_2} {f g : Y} (h : f = g) (x : X) :
f x = g x
theorem locally_constant.congr_arg {X : Type u_1} {Y : Type u_2} (f : Y) {x y : X} (h : x = y) :
f x = f y
theorem locally_constant.coe_injective {X : Type u_1} {Y : Type u_2}  :
@[simp, norm_cast]
theorem locally_constant.coe_inj {X : Type u_1} {Y : Type u_2} {f g : Y} :
f = g f = g
@[ext]
theorem locally_constant.ext {X : Type u_1} {Y : Type u_2} ⦃f g : Y⦄ (h : (x : X), f x = g x) :
f = g
theorem locally_constant.ext_iff {X : Type u_1} {Y : Type u_2} {f g : Y} :
f = g (x : X), f x = g x
@[protected]
theorem locally_constant.continuous {X : Type u_1} {Y : Type u_2} (f : Y) :
def locally_constant.to_continuous_map {X : Type u_1} {Y : Type u_2} (f : Y) :
C(X, Y)

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

Equations
@[protected, instance]
def locally_constant.continuous_map.has_coe {X : Type u_1} {Y : Type u_2}  :

As a shorthand, locally_constant.to_continuous_map is available as a coercion

Equations
@[simp]
theorem locally_constant.to_continuous_map_eq_coe {X : Type u_1} {Y : Type u_2} (f : Y) :
@[simp]
theorem locally_constant.coe_continuous_map {X : Type u_1} {Y : Type u_2} (f : Y) :
def locally_constant.const (X : Type u_1) {Y : Type u_2} (y : Y) :

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

Equations
@[simp]
theorem locally_constant.coe_const {X : Type u_1} {Y : Type u_2} (y : Y) :
def locally_constant.of_clopen {X : Type u_1} {U : set X} [Π (x : X), decidable (x U)] (hU : is_clopen U) :
(fin 2)

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

Equations
@[simp]
theorem locally_constant.of_clopen_fiber_zero {X : Type u_1} {U : set X} [Π (x : X), decidable (x U)] (hU : is_clopen U) :
⁻¹' {0} = U
@[simp]
theorem locally_constant.of_clopen_fiber_one {X : Type u_1} {U : set X} [Π (x : X), decidable (x U)] (hU : is_clopen U) :
⁻¹' {1} = U
theorem locally_constant.locally_constant_eq_of_fiber_zero_eq {X : Type u_1} (f g : (fin 2)) (h : f ⁻¹' {0} = g ⁻¹' {0}) :
f = g
theorem locally_constant.range_finite {X : Type u_1} {Y : Type u_2} (f : Y) :
theorem locally_constant.apply_eq_of_is_preconnected {X : Type u_1} {Y : Type u_2} (f : Y) {s : set X} (hs : is_preconnected s) {x y : X} (hx : x s) (hy : y s) :
f x = f y
theorem locally_constant.apply_eq_of_preconnected_space {X : Type u_1} {Y : Type u_2} (f : Y) (x y : X) :
f x = f y
theorem locally_constant.eq_const {X : Type u_1} {Y : Type u_2} (f : Y) (x : X) :
f = (f x)
theorem locally_constant.exists_eq_const {X : Type u_1} {Y : Type u_2} [nonempty Y] (f : Y) :
(y : Y),
def locally_constant.map {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : Y Z) :

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

Equations
@[simp]
theorem locally_constant.map_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : Y Z) (g : Y) :
g) = f g
@[simp]
theorem locally_constant.map_id {X : Type u_1} {Y : Type u_2}  :
@[simp]
theorem locally_constant.map_comp {X : Type u_1} {Y₁ : Type u_2} {Y₂ : Type u_3} {Y₃ : Type u_4} (g : Y₂ Y₃) (f : Y₁ Y₂) :
def locally_constant.flip {X : Type u_1} {α : Type u_2} {β : Type u_3} (f : β)) (a : α) :

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

Equations
def locally_constant.unflip {X : Type u_1} {α : Type u_2} {β : Type u_3} [fintype α] (f : α ) :
β)

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

Equations
@[simp]
theorem locally_constant.unflip_flip {X : Type u_1} {α : Type u_2} {β : Type u_3} [fintype α] (f : β)) :
@[simp]
theorem locally_constant.flip_unflip {X : Type u_1} {α : Type u_2} {β : Type u_3} [fintype α] (f : α ) :
noncomputable def locally_constant.comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : X Y) :

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
@[simp]
theorem locally_constant.coe_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : X Y) (g : Z) (hf : continuous f) :
@[simp]
theorem locally_constant.comap_id {X : Type u_1} {Z : Type u_3}  :
theorem locally_constant.comap_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {α : Type u_4} (f : X Y) (g : Y Z) (hf : continuous f) (hg : continuous g) :
theorem locally_constant.comap_const {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : X Y) (y : Y) (h : (x : X), f x = y) :
= λ (g : Z), {to_fun := λ (x : X), g y, is_locally_constant := _}
def locally_constant.desc {X : Type u_1} {α : Type u_2} {β : Type u_3} {g : α β} (f : X α) (h : β) (cond : g f = h) (inj : function.injective g) :

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

Equations
@[simp]
theorem locally_constant.coe_desc {X : Type u_1} {α : Type u_2} {β : Type u_3} (f : X α) (g : α β) (h : β) (cond : g f = h) (inj : function.injective g) :
cond inj) = f
@[simp]
theorem locally_constant.mul_indicator_apply {X : Type u_1} {R : Type u_5} [has_one R] {U : set X} (f : R) (hU : is_clopen U) (ᾰ : X) :
(f.mul_indicator hU) =
noncomputable def locally_constant.indicator {X : Type u_1} {R : Type u_5} [has_zero R] {U : set X} (f : R) (hU : is_clopen U) :

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.

Equations
noncomputable def locally_constant.mul_indicator {X : Type u_1} {R : Type u_5} [has_one R] {U : set X} (f : R) (hU : is_clopen U) :

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
@[simp]
theorem locally_constant.indicator_apply {X : Type u_1} {R : Type u_5} [has_zero R] {U : set X} (f : R) (hU : is_clopen U) (ᾰ : X) :
(f.indicator hU) = U.indicator f
theorem locally_constant.indicator_apply_eq_if {X : Type u_1} {R : Type u_5} [has_zero R] {U : set X} (f : R) (a : X) (hU : is_clopen U) :
(f.indicator hU) a = ite (a U) (f a) 0
theorem locally_constant.mul_indicator_apply_eq_if {X : Type u_1} {R : Type u_5} [has_one R] {U : set X} (f : R) (a : X) (hU : is_clopen U) :
(f.mul_indicator hU) a = ite (a U) (f a) 1
theorem locally_constant.mul_indicator_of_mem {X : Type u_1} {R : Type u_5} [has_one R] {U : set X} (f : R) {a : X} (hU : is_clopen U) (h : a U) :
(f.mul_indicator hU) a = f a
theorem locally_constant.indicator_of_mem {X : Type u_1} {R : Type u_5} [has_zero R] {U : set X} (f : R) {a : X} (hU : is_clopen U) (h : a U) :
(f.indicator hU) a = f a
theorem locally_constant.indicator_of_not_mem {X : Type u_1} {R : Type u_5} [has_zero R] {U : set X} (f : R) {a : X} (hU : is_clopen U) (h : a U) :
(f.indicator hU) a = 0
theorem locally_constant.mul_indicator_of_not_mem {X : Type u_1} {R : Type u_5} [has_one R] {U : set X} (f : R) {a : X} (hU : is_clopen U) (h : a U) :
(f.mul_indicator hU) a = 1