mathlib documentation

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 #

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
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 𝓝 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} [topological_space X] [discrete_topology X] (f : X → Y) :
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.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' Uf 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 𝓝 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' Uf x' = f x
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 𝓝 x, f y = f x
theorem is_locally_constant.continuous {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} (hf : is_locally_constant f) :
theorem is_locally_constant.iff_continuous {X : Type u_1} {Y : Type u_2} [topological_space X] {_x : topological_space Y} [discrete_topology Y] (f : X → Y) :
theorem is_locally_constant.iff_continuous_bot {X : Type u_1} {Y : Type u_2} [topological_space X] (f : X → Y) :
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.const {X : Type u_1} {Y : Type u_2} [topological_space X] (y : 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.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.range_finite {X : Type u_1} {Y : Type u_2} [topological_space X] [compact_space X] {f : X → Y} (hf : is_locally_constant f) :
theorem is_locally_constant.one {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] :
theorem is_locally_constant.zero {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero 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) :
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.

@[instance]
def locally_constant.has_coe_to_fun {X : Type u_1} {Y : Type u_2} [topological_space X] :
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
theorem locally_constant.coe_injective {X : Type u_1} {Y : Type u_2} [topological_space X] :
function.injective (λ (f : locally_constant X Y) (x : X), f x)
@[simp]
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
theorem locally_constant.continuous {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (f : locally_constant X Y) :
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
theorem locally_constant.range_finite {X : Type u_1} {Y : Type u_2} [topological_space X] [compact_space X] (f : locally_constant X Y) :
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
theorem locally_constant.apply_eq_of_preconnected_space {X : Type u_1} {Y : Type u_2} [topological_space X] [preconnected_space X] (f : locally_constant X Y) (x y : X) :
f x = f y
theorem locally_constant.eq_const {X : Type u_1} {Y : Type u_2} [topological_space X] [preconnected_space X] (f : locally_constant X Y) (x : X) :
theorem locally_constant.exists_eq_const {X : Type u_1} {Y : Type u_2} [topological_space X] [preconnected_space X] [nonempty Y] (f : locally_constant X Y) :
∃ (y : Y), f = locally_constant.const X 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]
theorem locally_constant.map_id {X : Type u_1} {Y : Type u_2} [topological_space X] :
@[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.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) :
@[simp]
theorem locally_constant.comap_id {X : Type u_1} {Z : Type u_3} [topological_space X] :
theorem locally_constant.comap_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {α : Type u_4} [topological_space X] [topological_space Y] [topological_space Z] (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} [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 := _}