# mathlibdocumentation

topology.locally_constant.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 #

• 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
theorem is_locally_constant.tfae {X : Type u_1} {Y : Type u_2} (f : X → Y) :
, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 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' Uf 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' Uf 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 𝓝 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' Uf x' = f x
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 𝓝 x, f y = f x
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.iff_continuous_bot {X : Type u_1} {Y : Type u_2} (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.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.

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.

@[instance]
def locally_constant.inhabited {X : Type u_1} {Y : Type u_2} [inhabited Y] :
Equations
@[instance]
def locally_constant.has_coe_to_fun {X : Type u_1} {Y : Type u_2}  :
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]
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
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
@[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) :
theorem locally_constant.to_continuous_map_injective {X : Type u_1} {Y : Type u_2}  :
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 : α → ) :
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