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 mapf : X → YwhereXis a topological space is locally constant if every set inYhas an open preimage.locally_constant X Y: the type of locally constant maps fromXtoYlocally_constant.map: push-forward of locally constant mapslocally_constant.comap: pull-back of locally constant maps
A function between topological spaces is locally constant if the preimage of any set is open.
Equations
- is_locally_constant f = ∀ (s : set Y), is_open (f ⁻¹' s)
@[protected]
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) :
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) :
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) :
theorem
is_locally_constant.iff_exists_open
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
(f : X → Y) :
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) :
@[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) :
@[protected]
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.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) :
is_locally_constant (g ∘ f)
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) :
is_locally_constant (g ∘ 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.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) :
is_locally_constant (f + 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) :
is_locally_constant (f * 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) :
is_locally_constant (f / 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) :
is_locally_constant (f - 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.
- to_fun : X → Y
- is_locally_constant : is_locally_constant self.to_fun
A (bundled) locally constant function from a topological space X to a type Y.
@[protected, instance]
def
locally_constant.inhabited
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[inhabited Y] :
inhabited (locally_constant X Y)
Equations
- locally_constant.inhabited = {default := {to_fun := function.const X default, is_locally_constant := _}}
@[protected, instance]
def
locally_constant.has_coe_to_fun
{X : Type u_1}
{Y : Type u_2}
[topological_space X] :
has_coe_to_fun (locally_constant X Y) (λ (_x : locally_constant X Y), X → Y)
Equations
- locally_constant.has_coe_to_fun = {coe := locally_constant.to_fun _inst_1}
@[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) :
⇑{to_fun := f, is_locally_constant := h} = 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) :
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) :
@[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} :
@[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} :
@[protected]
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.to_continuous_map
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
(f : locally_constant X Y) :
We can turn a locally-constant function into a bundled continuous_map.
Equations
- f.to_continuous_map = {to_fun := ⇑f, continuous_to_fun := _}
@[protected, instance]
def
locally_constant.continuous_map.has_coe
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y] :
has_coe (locally_constant X Y) C(X, Y)
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}
[topological_space X]
[topological_space Y]
(f : locally_constant X Y) :
f.to_continuous_map = ↑f
@[simp]
theorem
locally_constant.coe_continuous_map
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
(f : locally_constant X Y) :
theorem
locally_constant.to_continuous_map_injective
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y] :
def
locally_constant.const
(X : Type u_1)
{Y : Type u_2}
[topological_space X]
(y : Y) :
locally_constant X Y
The constant locally constant function on X with value y : Y.
Equations
- locally_constant.const X y = {to_fun := function.const X y, is_locally_constant := _}
@[simp]
theorem
locally_constant.coe_const
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
(y : Y) :
⇑(locally_constant.const X y) = function.const X 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) :
locally_constant X (fin 2)
The locally constant function to fin 2 associated to a clopen set.
Equations
- locally_constant.of_clopen hU = {to_fun := λ (x : X), ite (x ∈ U) 0 1, is_locally_constant := _}
@[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) :
⇑(locally_constant.of_clopen hU) ⁻¹' {0} = 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) :
⇑(locally_constant.of_clopen hU) ⁻¹' {1} = Uᶜ
theorem
locally_constant.locally_constant_eq_of_fiber_zero_eq
{X : Type u_1}
[topological_space X]
(f g : locally_constant X (fin 2))
(h : ⇑f ⁻¹' {0} = ⇑g ⁻¹' {0}) :
f = g
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) :
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) :
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) :
f = locally_constant.const X (⇑f 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) :
locally_constant X Y → locally_constant X Z
Push forward of locally constant maps under any map, by post-composition.
Equations
- locally_constant.map f = λ (g : locally_constant X Y), {to_fun := f ∘ ⇑g, is_locally_constant := _}
@[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) :
⇑(locally_constant.map f g) = f ∘ ⇑g
@[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 : α) :
locally_constant X β
Given a locally constant function to α → β, construct a family of locally constant
functions with values in β indexed by α.
Equations
- f.flip a = locally_constant.map (λ (f : α → β), f a) f
def
locally_constant.unflip
{X : Type u_1}
{α : Type u_2}
{β : Type u_3}
[fintype α]
[topological_space X]
(f : α → locally_constant X β) :
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
- locally_constant.unflip f = {to_fun := λ (x : X) (a : α), ⇑(f a) x, is_locally_constant := _}
@[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 β) :
(locally_constant.unflip f).flip = f
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) :
locally_constant Y Z → locally_constant X Z
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
- locally_constant.comap f = dite (continuous f) (λ (hf : continuous f) (g : locally_constant Y Z), {to_fun := ⇑g ∘ f, is_locally_constant := _}) (λ (hf : ¬continuous f), dite (nonempty X) (λ (H : nonempty X) (g : locally_constant Y Z), locally_constant.const X (⇑g (f (classical.arbitrary X)))) (λ (H : ¬nonempty X) (g : locally_constant Y Z), {to_fun := λ (x : X), _.elim, is_locally_constant := _}))
@[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) :
⇑(locally_constant.comap f g) = ⇑g ∘ f
@[simp]
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 := _}
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) :
locally_constant X α
If a locally constant function factors through an injection, then it factors through a locally constant function.
Equations
- locally_constant.desc f h cond inj = {to_fun := f, is_locally_constant := _}
@[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