topology.locally_constant.basic

source

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

is_locally_constant f = ∀ (s : set Y), is_open (f ⁻¹' s)

source

@[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

source

theorem is_locally_constant.of_discrete {X : Type u_1} {Y : Type u_2} [topological_space X] [discrete_topology X] (f : X → Y) :

is_locally_constant f

source

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}

source

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}

source

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}

source

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

source

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

source

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

source

@[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

source

@[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) :

continuous f

source

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) :

is_locally_constant f ↔ continuous f

source

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) :

is_locally_constant f

source

theorem is_locally_constant.const {X : Type u_1} {Y : Type u_2} [topological_space X] (y : Y) :

is_locally_constant (function.const X y)

source

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)

source

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))

source

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))

source

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)

source

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.

source

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

source

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)

source

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

source

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

source

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) :

(set.range f).finite

source

theorem is_locally_constant.one {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] :

is_locally_constant 1

source

theorem is_locally_constant.zero {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero Y] :

is_locally_constant 0

source

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) :

is_locally_constant (-f)

source

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) :

is_locally_constant f⁻¹

source

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)

source

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)

source

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)

source

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)

source

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) :

is_locally_constant f

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

source

theorem is_locally_constant.of_constant_on_connected_components {X : Type u_1} {Y : Type u_2} [topological_space X] [locally_connected_space X] {f : X → Y} (h : ∀ (x y : X), y ∈ connected_component x → f y = f x) :

is_locally_constant f

source

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) :

is_locally_constant f

source

structure locally_constant (X : Type u_5) (Y : Type u_6) [topological_space X] :

Type (max u_5 u_6)

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.

Instances for locally_constant

source

@[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 inhabited.default, is_locally_constant := _}}

source

@[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}

source

@[simp]

theorem locally_constant.to_fun_eq_coe {X : Type u_1} {Y : Type u_2} [topological_space X] (f : locally_constant X Y) :

f.to_fun = ⇑f

source

@[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

source

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

source

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

source

theorem locally_constant.coe_injective {X : Type u_1} {Y : Type u_2} [topological_space X] :

function.injective coe_fn

source

@[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

source

@[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

source

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

source

@[protected]

theorem locally_constant.continuous {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (f : locally_constant X Y) :

continuous ⇑f

source

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) :

C(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 := _}

source

@[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

locally_constant.continuous_map.has_coe = {coe := locally_constant.to_continuous_map _inst_2}

source

@[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

source

@[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) :

⇑↑f = ⇑f

source

theorem locally_constant.to_continuous_map_injective {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] :

function.injective locally_constant.to_continuous_map

source

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 := _}

source

@[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

source

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 := _}

source

@[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

source

@[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ᶜ

source

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

source

theorem locally_constant.range_finite {X : Type u_1} {Y : Type u_2} [topological_space X] [compact_space X] (f : locally_constant X Y) :

(set.range ⇑f).finite

source

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

source

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

source

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)

source

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

source

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 := _}

source

@[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

source

@[simp]

theorem locally_constant.map_id {X : Type u_1} {Y : Type u_2} [topological_space X] :

locally_constant.map id = id

source

@[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₂) :

locally_constant.map g ∘ locally_constant.map f = locally_constant.map (g ∘ f)

source

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

source

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 := _}

source

@[simp]

theorem locally_constant.unflip_flip {X : Type u_1} {α : Type u_2} {β : Type u_3} [fintype α] [topological_space X] (f : locally_constant X (α → β)) :

locally_constant.unflip f.flip = f

source

@[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

source

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 := _}))

source

@[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

source

@[simp]

theorem locally_constant.comap_id {X : Type u_1} {Z : Type u_3} [topological_space X] :

locally_constant.comap id = id

source

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) :

locally_constant.comap f ∘ locally_constant.comap g = locally_constant.comap (g ∘ f)

source

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 := _}

source

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 := _}

source

@[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

source

@[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) :

⇑(f.mul_indicator hU) ᾰ = U.mul_indicator ⇑f ᾰ

source

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) :

locally_constant X R

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

f.indicator hU = {to_fun := U.indicator ⇑f, is_locally_constant := _}

source

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) :

locally_constant X R

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

f.mul_indicator hU = {to_fun := U.mul_indicator ⇑f, is_locally_constant := _}

source

@[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 ᾰ

source

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

source

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

source

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

source

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

source

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

source

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

mathlib3 documentation

Locally constant functions #

Main definitions and constructions #