mathlib3 documentation

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 #

def is_locally_constant {X : Type u_1} {Y : Type u_2} [topological_space X] (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} [topological_space X] (f : X Y) :
[is_locally_constant f, (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.is_open_fiber {X : Type u_1} {Y : Type u_2} [topological_space X] {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} [topological_space X] {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} [topological_space X] {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} [topological_space X] (f : X Y) :
is_locally_constant f (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} [topological_space X] (f : X Y) :
is_locally_constant f (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} [topological_space X] {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} [topological_space X] {f : X Y} (hf : is_locally_constant f) (x : X) :
∀ᶠ (y : X) in nhds x, f y = f x
@[protected]
theorem is_locally_constant.of_constant {X : Type u_1} {Y : Type u_2} [topological_space X] (f : X Y) (h : (x y : X), f x = f y) :
theorem is_locally_constant.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] {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} [topological_space X] {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} [topological_space X] {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} [topological_space X] [topological_space Y] {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} [topological_space X] {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} [topological_space X] [preconnected_space X] {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} [topological_space X] [preconnected_space X] {f : X Y} (hf : is_locally_constant f) (x : X) :
f = function.const X (f x)
theorem is_locally_constant.exists_eq_const {X : Type u_1} {Y : Type u_2} [topological_space X] [preconnected_space X] [nonempty Y] {f : X Y} (hf : is_locally_constant f) :
(y : Y), f = function.const X y
theorem is_locally_constant.iff_is_const {X : Type u_1} {Y : Type u_2} [topological_space X] [preconnected_space X] {f : X Y} :
is_locally_constant f (x y : X), f x = f y
theorem is_locally_constant.neg {X : Type u_1} {Y : Type u_2} [topological_space X] [has_neg Y] ⦃f : X Y⦄ (hf : is_locally_constant f) :
theorem is_locally_constant.inv {X : Type u_1} {Y : Type u_2} [topological_space X] [has_inv Y] ⦃f : X Y⦄ (hf : is_locally_constant f) :
theorem is_locally_constant.add {X : Type u_1} {Y : Type u_2} [topological_space X] [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} [topological_space X] [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} [topological_space X] [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} [topological_space X] [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} [topological_space X] {α : 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_preconnected_clopens {X : Type u_1} {Y : Type u_2} [topological_space X] [locally_connected_space X] {f : X Y} (h : (U : set X), is_preconnected U is_clopen U (x : X), x U (y : X), y U f y = f x) :
structure locally_constant (X : Type u_5) (Y : Type u_6) [topological_space X] :
Type (max u_5 u_6)

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

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

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

Equations
def locally_constant.const (X : Type u_1) {Y : Type u_2} [topological_space X] (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} [topological_space X] (y : Y) :
def locally_constant.of_clopen {X : Type u_1} [topological_space X] {U : set X} [Π (x : X), decidable (x U)] (hU : is_clopen U) :

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} [topological_space X] {U : set X} [Π (x : X), decidable (x U)] (hU : is_clopen U) :
@[simp]
theorem locally_constant.of_clopen_fiber_one {X : Type u_1} [topological_space X] {U : set X} [Π (x : X), decidable (x U)] (hU : is_clopen U) :
theorem locally_constant.apply_eq_of_is_preconnected {X : Type u_1} {Y : Type u_2} [topological_space X] (f : locally_constant X Y) {s : set X} (hs : is_preconnected s) {x y : X} (hx : x s) (hy : y s) :
f x = f y
def locally_constant.map {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] (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} [topological_space X] (f : Y Z) (g : locally_constant X Y) :
@[simp]
@[simp]
theorem locally_constant.map_comp {X : Type u_1} [topological_space X] {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} [topological_space X] (f : locally_constant X β)) (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 α] [topological_space X] (f : α locally_constant X β) :

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 α] [topological_space X] (f : locally_constant X β)) :
@[simp]
theorem locally_constant.flip_unflip {X : Type u_1} {α : Type u_2} {β : Type u_3} [fintype α] [topological_space X] (f : α locally_constant X β) :
noncomputable def locally_constant.comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] (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} [topological_space X] [topological_space Y] (f : X Y) (g : locally_constant Y Z) (hf : continuous f) :
theorem locally_constant.comap_const {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] (f : X Y) (y : Y) (h : (x : X), f x = y) :
locally_constant.comap f = λ (g : locally_constant Y Z), {to_fun := λ (x : X), g y, is_locally_constant := _}
def locally_constant.desc {X : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space X] {g : α β} (f : X α) (h : locally_constant X β) (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} [topological_space X] (f : X α) (g : α β) (h : locally_constant X β) (cond : g f = h) (inj : function.injective g) :
(locally_constant.desc f h cond inj) = f
@[simp]
theorem locally_constant.mul_indicator_apply {X : Type u_1} [topological_space X] {R : Type u_5} [has_one R] {U : set X} (f : locally_constant X R) (hU : is_clopen U) (ᾰ : X) :
noncomputable def locally_constant.indicator {X : Type u_1} [topological_space X] {R : Type u_5} [has_zero R] {U : set X} (f : locally_constant X 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} [topological_space X] {R : Type u_5} [has_one R] {U : set X} (f : locally_constant X 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} [topological_space X] {R : Type u_5} [has_zero R] {U : set X} (f : locally_constant X R) (hU : is_clopen U) (ᾰ : X) :
(f.indicator hU) = U.indicator f
theorem locally_constant.indicator_apply_eq_if {X : Type u_1} [topological_space X] {R : Type u_5} [has_zero R] {U : set X} (f : locally_constant X 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} [topological_space X] {R : Type u_5} [has_one R] {U : set X} (f : locally_constant X 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} [topological_space X] {R : Type u_5} [has_one R] {U : set X} (f : locally_constant X 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} [topological_space X] {R : Type u_5} [has_zero R] {U : set X} (f : locally_constant X 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} [topological_space X] {R : Type u_5} [has_zero R] {U : set X} (f : locally_constant X 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} [topological_space X] {R : Type u_5} [has_one R] {U : set X} (f : locally_constant X R) {a : X} (hU : is_clopen U) (h : a U) :
(f.mul_indicator hU) a = 1