Locally constant functions

This file sets up the theory of locally constant function from a topological space to a type.

Main definitions and constructions

• IsLocallyConstant f : a map f : X → Y where X is a topological space is locally constant if every set in Y has an open preimage.
• LocallyConstant X Y : the type of locally constant maps from X to Y
• LocallyConstant.map : push-forward of locally constant maps
• LocallyConstant.comap : pull-back of locally constant maps

def IsLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : X → Y) : Prop

A function between topological spaces is locally constant if the preimage of any set is open.

theorem IsLocallyConstant.tfae {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : X → Y) : List.TFAE [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in nhds x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x}, ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x]

theorem IsLocallyConstant.of_discrete {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [DiscreteTopology X] (f : X → Y) : IsLocallyConstant f

theorem IsLocallyConstant.isOpen_fiber {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} (hf : IsLocallyConstant f) (y : Y) : IsOpen {x | f x = y}

theorem IsLocallyConstant.isClosed_fiber {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} (hf : IsLocallyConstant f) (y : Y) : IsClosed {x | f x = y}

theorem IsLocallyConstant.isClopen_fiber {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} (hf : IsLocallyConstant f) (y : Y) : IsClopen {x | f x = y}

theorem IsLocallyConstant.iff_exists_open {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : X → Y) : IsLocallyConstant f ↔ ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x

theorem IsLocallyConstant.iff_eventually_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : X → Y) : IsLocallyConstant f ↔ ∀ (x : X), ∀ᶠ (y : X) in nhds x, f y = f x

theorem IsLocallyConstant.exists_open {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} (hf : IsLocallyConstant f) (x : X) : ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ (x' : X), x' ∈ U → f x' = f x

theorem IsLocallyConstant.eventually_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} (hf : IsLocallyConstant f) (x : X) : ∀ᶠ (y : X) in nhds x, f y = f x

theorem IsLocallyConstant.iff_isOpen_fiber_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} : IsLocallyConstant f ↔ ∀ (x : X), IsOpen (f ⁻¹' {f x})

theorem IsLocallyConstant.iff_isOpen_fiber {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} : IsLocallyConstant f ↔ ∀ (y : Y), IsOpen (f ⁻¹' {y})

theorem IsLocallyConstant.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocallyConstant f) : Continuous f

theorem IsLocallyConstant.iff_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] : ∀ {x : TopologicalSpace Y} [inst : DiscreteTopology Y] (f : X → Y), IsLocallyConstant f ↔ Continuous f

theorem IsLocallyConstant.of_constant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : X → Y) (h : ∀ (x y : X), f x = f y) : IsLocallyConstant f

theorem IsLocallyConstant.const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (y : Y) : IsLocallyConstant (Function.const X y)

theorem IsLocallyConstant.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] {f : X → Y} (hf : IsLocallyConstant f) (g : Y → Z) : IsLocallyConstant (g ∘ f)

theorem IsLocallyConstant.prod_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Y' : Type u_5} {f : X → Y} {f' : X → Y'} (hf : IsLocallyConstant f) (hf' : IsLocallyConstant f') : IsLocallyConstant fun x => (f x, f' x)

theorem IsLocallyConstant.comp₂ {X : Type u_1} [TopologicalSpace X] {Y₁ : Type u_5} {Y₂ : Type u_6} {Z : Type u_7} {f : X → Y₁} {g : X → Y₂} (hf : IsLocallyConstant f) (hg : IsLocallyConstant g) (h : Y₁ → Y₂ → Z) : IsLocallyConstant fun x => h (f x) (g x)

theorem IsLocallyConstant.comp_continuous {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {g : Y → Z} {f : X → Y} (hg : IsLocallyConstant g) (hf : Continuous f) : IsLocallyConstant (g ∘ f)

theorem IsLocallyConstant.apply_eq_of_isPreconnected {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} (hf : IsLocallyConstant f) {s : Set X} (hs : IsPreconnected s) {x : X} {y : X} (hx : x ∈ s) (hy : y ∈ s) : f x = f y

A locally constant function is constant on any preconnected set.

theorem IsLocallyConstant.apply_eq_of_preconnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] {f : X → Y} (hf : IsLocallyConstant f) (x : X) (y : X) : f x = f y

theorem IsLocallyConstant.eq_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] {f : X → Y} (hf : IsLocallyConstant f) (x : X) : f = Function.const X (f x)

theorem IsLocallyConstant.exists_eq_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] [Nonempty Y] {f : X → Y} (hf : IsLocallyConstant f) : ∃ y, f = Function.const X y

theorem IsLocallyConstant.iff_is_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] {f : X → Y} : IsLocallyConstant f ↔ ∀ (x y : X), f x = f y

theorem IsLocallyConstant.range_finite {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CompactSpace X] {f : X → Y} (hf : IsLocallyConstant f) : Set.Finite (Set.range f)

theorem IsLocallyConstant.zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Zero Y] : IsLocallyConstant 0

theorem IsLocallyConstant.one {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [One Y] : IsLocallyConstant 1

theorem IsLocallyConstant.neg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Neg Y] ⦃f : X → Y⦄ (hf : IsLocallyConstant f) : IsLocallyConstant (-f)

theorem IsLocallyConstant.inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Inv Y] ⦃f : X → Y⦄ (hf : IsLocallyConstant f) : IsLocallyConstant f⁻¹

theorem IsLocallyConstant.add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Add Y] ⦃f : X → Y⦄ ⦃g : X → Y⦄ (hf : IsLocallyConstant f) (hg : IsLocallyConstant g) : IsLocallyConstant (f + g)

theorem IsLocallyConstant.mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Mul Y] ⦃f : X → Y⦄ ⦃g : X → Y⦄ (hf : IsLocallyConstant f) (hg : IsLocallyConstant g) : IsLocallyConstant (f * g)

theorem IsLocallyConstant.sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Sub Y] ⦃f : X → Y⦄ ⦃g : X → Y⦄ (hf : IsLocallyConstant f) (hg : IsLocallyConstant g) : IsLocallyConstant (f - g)

theorem IsLocallyConstant.div {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Div Y] ⦃f : X → Y⦄ ⦃g : X → Y⦄ (hf : IsLocallyConstant f) (hg : IsLocallyConstant g) : IsLocallyConstant (f / g)

theorem IsLocallyConstant.desc {X : Type u_1} [TopologicalSpace X] {α : Type u_5} {β : Type u_6} (f : X → α) (g : α → β) (h : IsLocallyConstant (g ∘ f)) (inj : Function.Injective g) : IsLocallyConstant f

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

theorem IsLocallyConstant.of_constant_on_connected_components {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LocallyConnectedSpace X] {f : X → Y} (h : ∀ (x y : X), y ∈ connectedComponent x → f y = f x) : IsLocallyConstant f

theorem IsLocallyConstant.of_constant_on_connected_clopens {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LocallyConnectedSpace X] {f : X → Y} (h : ∀ (U : Set X), IsConnected U → IsClopen U → ∀ (x : X), x ∈ U → ∀ (y : X), y ∈ U → f y = f x) : IsLocallyConstant f

theorem IsLocallyConstant.of_constant_on_preconnected_clopens {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LocallyConnectedSpace X] {f : X → Y} (h : ∀ (U : Set X), IsPreconnected U → IsClopen U → ∀ (x : X), x ∈ U → ∀ (y : X), y ∈ U → f y = f x) : IsLocallyConstant f

structure LocallyConstant (X : Type u_5) (Y : Type u_6) [TopologicalSpace X] : Type (max u_5 u_6)

• toFun : X → Y

  The underlying function.

• isLocallyConstant : IsLocallyConstant s.toFun

  The map is locally constant.

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

instance LocallyConstant.instInhabitedLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Inhabited Y] : Inhabited (LocallyConstant X Y)

instance LocallyConstant.instFunLikeLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] : FunLike (LocallyConstant X Y) X fun x => Y

def LocallyConstant.Simps.apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : LocallyConstant X Y) : X → Y

See Note [custom simps projections].

@[simp]

theorem LocallyConstant.toFun_eq_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : LocallyConstant X Y) : f.toFun = ↑f

@[simp]

theorem LocallyConstant.coe_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : X → Y) (h : IsLocallyConstant f) : ↑{ toFun := f, isLocallyConstant := h } = f

theorem LocallyConstant.congr_fun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : LocallyConstant X Y} {g : LocallyConstant X Y} (h : f = g) (x : X) : ↑f x = ↑g x

theorem LocallyConstant.congr_arg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : LocallyConstant X Y) {x : X} {y : X} (h : x = y) : ↑f x = ↑f y

theorem LocallyConstant.coe_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] : Function.Injective FunLike.coe

theorem LocallyConstant.coe_inj {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : LocallyConstant X Y} {g : LocallyConstant X Y} : ↑f = ↑g ↔ f = g

theorem LocallyConstant.ext {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] ⦃f : LocallyConstant X Y⦄ ⦃g : LocallyConstant X Y⦄ (h : ∀ (x : X), ↑f x = ↑g x) : f = g

theorem LocallyConstant.ext_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : LocallyConstant X Y} {g : LocallyConstant X Y} : f = g ↔ ∀ (x : X), ↑f x = ↑g x

theorem LocallyConstant.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : LocallyConstant X Y) : Continuous ↑f

def LocallyConstant.toContinuousMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : LocallyConstant X Y) : C(X, Y)

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

instance LocallyConstant.instCoeLocallyConstantContinuousMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : Coe (LocallyConstant X Y) C(X, Y)

As a shorthand, LocallyConstant.toContinuousMap is available as a coercion

@[simp]

theorem LocallyConstant.coe_continuousMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : LocallyConstant X Y) : ↑↑f = ↑f

theorem LocallyConstant.toContinuousMap_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : Function.Injective LocallyConstant.toContinuousMap

def LocallyConstant.const (X : Type u_5) {Y : Type u_6} [TopologicalSpace X] (y : Y) : LocallyConstant X Y

The constant locally constant function on X with value y : Y.

@[simp]

theorem LocallyConstant.coe_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (y : Y) : ↑(LocallyConstant.const X y) = Function.const X y

def LocallyConstant.ofClopen {X : Type u_5} [TopologicalSpace X] {U : Set X} [(x : X) → Decidable (x ∈ U)] (hU : IsClopen U) : LocallyConstant X (Fin 2)

The locally constant function to Fin 2 associated to a clopen set.

@[simp]

theorem LocallyConstant.ofClopen_fiber_zero {X : Type u_5} [TopologicalSpace X] {U : Set X} [(x : X) → Decidable (x ∈ U)] (hU : IsClopen U) : ↑(LocallyConstant.ofClopen hU) ⁻¹' {0} = U

@[simp]

theorem LocallyConstant.ofClopen_fiber_one {X : Type u_5} [TopologicalSpace X] {U : Set X} [(x : X) → Decidable (x ∈ U)] (hU : IsClopen U) : ↑(LocallyConstant.ofClopen hU) ⁻¹' {1} = Uᶜ

theorem LocallyConstant.locallyConstant_eq_of_fiber_zero_eq {X : Type u_5} [TopologicalSpace X] (f : LocallyConstant X (Fin 2)) (g : LocallyConstant X (Fin 2)) (h : ↑f ⁻¹' {0} = ↑g ⁻¹' {0}) : f = g

theorem LocallyConstant.range_finite {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CompactSpace X] (f : LocallyConstant X Y) : Set.Finite (Set.range ↑f)

theorem LocallyConstant.apply_eq_of_isPreconnected {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : LocallyConstant X Y) {s : Set X} (hs : IsPreconnected s) {x : X} {y : X} (hx : x ∈ s) (hy : y ∈ s) : ↑f x = ↑f y

theorem LocallyConstant.apply_eq_of_preconnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] (f : LocallyConstant X Y) (x : X) (y : X) : ↑f x = ↑f y

theorem LocallyConstant.eq_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] (f : LocallyConstant X Y) (x : X) : f = LocallyConstant.const X (↑f x)

theorem LocallyConstant.exists_eq_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PreconnectedSpace X] [Nonempty Y] (f : LocallyConstant X Y) : ∃ y, f = LocallyConstant.const X y

def LocallyConstant.map {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (f : Y → Z) (g : LocallyConstant X Y) : LocallyConstant X Z

Push forward of locally constant maps under any map, by post-composition.

@[simp]

theorem LocallyConstant.map_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (f : Y → Z) (g : LocallyConstant X Y) : ↑(LocallyConstant.map f g) = f ∘ ↑g

@[simp]

theorem LocallyConstant.map_id {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] : LocallyConstant.map id = id

@[simp]

theorem LocallyConstant.map_comp {X : Type u_1} [TopologicalSpace X] {Y₁ : Type u_5} {Y₂ : Type u_6} {Y₃ : Type u_7} (g : Y₂ → Y₃) (f : Y₁ → Y₂) : LocallyConstant.map g ∘ LocallyConstant.map f = LocallyConstant.map (g ∘ f)

def LocallyConstant.flip {X : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace X] (f : LocallyConstant X (α → β)) (a : α) : LocallyConstant X β

Given a locally constant function to α → β, construct a family of locally constant functions with values in β indexed by α.

def LocallyConstant.unflip {X : Type u_5} {α : Type u_6} {β : Type u_7} [Finite α] [TopologicalSpace X] (f : α → LocallyConstant X β) : LocallyConstant X (α → β)

If α is finite, this constructs a locally constant function to α → β given a family of locally constant functions with values in β indexed by α.

@[simp]

theorem LocallyConstant.unflip_flip {X : Type u_5} {α : Type u_6} {β : Type u_7} [Finite α] [TopologicalSpace X] (f : LocallyConstant X (α → β)) : LocallyConstant.unflip (LocallyConstant.flip f) = f

@[simp]

theorem LocallyConstant.flip_unflip {X : Type u_5} {α : Type u_6} {β : Type u_7} [Finite α] [TopologicalSpace X] (f : α → LocallyConstant X β) : LocallyConstant.flip (LocallyConstant.unflip f) = f

noncomputable def LocallyConstant.comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : LocallyConstant Y Z → LocallyConstant 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 LocallyConstant.coe_comap.

TODO: take f : C(X, Y) as an argument? Or we actually use it for discontinuous f?

@[simp]

theorem LocallyConstant.coe_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (g : LocallyConstant Y Z) (hf : Continuous f) : ↑(LocallyConstant.comap f g) = ↑g ∘ f

theorem LocallyConstant.coe_comap_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (g : LocallyConstant Y Z) (hf : Continuous f) (x : X) : ↑(LocallyConstant.comap f g) x = ↑g (f x)

@[simp]

theorem LocallyConstant.comap_id {X : Type u_1} {Z : Type u_3} [TopologicalSpace X] : LocallyConstant.comap id = id

theorem LocallyConstant.comap_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X → Y) (g : Y → Z) (hf : Continuous f) (hg : Continuous g) : LocallyConstant.comap f ∘ LocallyConstant.comap g = LocallyConstant.comap (g ∘ f)

theorem LocallyConstant.comap_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X → Y) (g : Y → Z) (hf : Continuous f) (hg : Continuous g) (x : LocallyConstant Z α) : LocallyConstant.comap f (LocallyConstant.comap g x) = LocallyConstant.comap (g ∘ f) x

theorem LocallyConstant.comap_const {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (y : Y) (h : ∀ (x : X), f x = y) : LocallyConstant.comap f = fun g => LocallyConstant.const X (↑g y)

theorem LocallyConstant.comap_injective {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : Continuous f) (hfs : Function.Surjective f) : Function.Injective (LocallyConstant.comap f)

def LocallyConstant.desc {X : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace X] {g : α → β} (f : X → α) (h : LocallyConstant X β) (cond : g ∘ f = ↑h) (inj : Function.Injective g) : LocallyConstant X α

If a locally constant function factors through an injection, then it factors through a locally constant function.

@[simp]

theorem LocallyConstant.coe_desc {X : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace X] (f : X → α) (g : α → β) (h : LocallyConstant X β) (cond : g ∘ f = ↑h) (inj : Function.Injective g) : ↑(LocallyConstant.desc f h cond inj) = f

theorem LocallyConstant.indicator.proof_1 {X : Type u_2} [TopologicalSpace X] {R : Type u_1} [Zero R] {U : Set X} (f : LocallyConstant X R) (hU : IsClopen U) (s : Set R) : IsOpen (Set.indicator U ↑f ⁻¹' s)

noncomputable def LocallyConstant.indicator {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [Zero R] {U : Set X} (f : LocallyConstant X R) (hU : IsClopen U) : LocallyConstant 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.

@[simp]

theorem LocallyConstant.mulIndicator_apply {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [One R] {U : Set X} (f : LocallyConstant X R) (hU : IsClopen U) (x : X) : ↑(LocallyConstant.mulIndicator f hU) x = Set.mulIndicator U (↑f) x

@[simp]

theorem LocallyConstant.indicator_apply {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [Zero R] {U : Set X} (f : LocallyConstant X R) (hU : IsClopen U) (x : X) : ↑(LocallyConstant.indicator f hU) x = Set.indicator U (↑f) x

noncomputable def LocallyConstant.mulIndicator {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [One R] {U : Set X} (f : LocallyConstant X R) (hU : IsClopen U) : LocallyConstant X R

Given a clopen set U and a locally constant function f, LocallyConstant.mulIndicator returns the locally constant function that is f on U and 1 otherwise.

theorem LocallyConstant.indicator_apply_eq_if {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [Zero R] {U : Set X} (f : LocallyConstant X R) (a : X) (hU : IsClopen U) : ↑(LocallyConstant.indicator f hU) a = if a ∈ U then ↑f a else 0

theorem LocallyConstant.mulIndicator_apply_eq_if {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [One R] {U : Set X} (f : LocallyConstant X R) (a : X) (hU : IsClopen U) : ↑(LocallyConstant.mulIndicator f hU) a = if a ∈ U then ↑f a else 1

theorem LocallyConstant.indicator_of_mem {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [Zero R] {U : Set X} (f : LocallyConstant X R) {a : X} (hU : IsClopen U) (h : a ∈ U) : ↑(LocallyConstant.indicator f hU) a = ↑f a

theorem LocallyConstant.mulIndicator_of_mem {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [One R] {U : Set X} (f : LocallyConstant X R) {a : X} (hU : IsClopen U) (h : a ∈ U) : ↑(LocallyConstant.mulIndicator f hU) a = ↑f a

theorem LocallyConstant.indicator_of_not_mem {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [Zero R] {U : Set X} (f : LocallyConstant X R) {a : X} (hU : IsClopen U) (h : ¬a ∈ U) : ↑(LocallyConstant.indicator f hU) a = 0

theorem LocallyConstant.mulIndicator_of_not_mem {X : Type u_1} [TopologicalSpace X] {R : Type u_5} [One R] {U : Set X} (f : LocallyConstant X R) {a : X} (hU : IsClopen U) (h : ¬a ∈ U) : ↑(LocallyConstant.mulIndicator f hU) a = 1

@[simp]

theorem LocallyConstant.congrLeft_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : ∀ (a : LocallyConstant X Z), ↑(LocallyConstant.congrLeft e) a = LocallyConstant.comap (↑(Homeomorph.symm e)) a

@[simp]

theorem LocallyConstant.congrLeft_symm_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : ∀ (a : LocallyConstant Y Z), ↑(LocallyConstant.congrLeft e).symm a = LocallyConstant.comap (↑e) a

noncomputable def LocallyConstant.congrLeft {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : LocallyConstant X Z ≃ LocallyConstant Y Z

The equivalence between LocallyConstant X Z and LocallyConstant Y Z given a homeomorphism X ≃ₜ Y

def LocallyConstant.piecewise {X : Type u_1} {Z : Type u_3} [TopologicalSpace X] {C₁ : Set X} {C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂) (h : C₁ ∪ C₂ = Set.univ) (f : LocallyConstant (↑C₁) Z) (g : LocallyConstant (↑C₂) Z) (hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), LocallyConstant.toFun f { val := x, property := (_ : x ∈ C₁) } = LocallyConstant.toFun g { val := x, property := (_ : x ∈ C₂) }) [(j : X) → Decidable (j ∈ C₁)] : LocallyConstant X Z

Given two closed sets covering a topological space, and locally constant maps on these two sets, then if these two locally constant maps agree on the intersection, we get a piecewise defined locally constant map on the whole space.