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.

Equations

• IsLocallyConstant f = ∀ (s : Set Y), IsOpen (f ⁻¹' s)

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' : X | f x' = f x}, ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ ∀ 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 : 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 : 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 : 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 : Set X), IsOpen U ∧ x ∈ U ∧ ∀ 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 : Set X), IsOpen U ∧ x ∈ U ∧ ∀ 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 : 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 : 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 : 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 ∈ U, ∀ 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 ∈ U, ∀ 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)

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

• toFun : X → Y

  The underlying function.

• isLocallyConstant : IsLocallyConstant self.toFun

  The map is locally constant.

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

Equations

• LocallyConstant.instInhabitedLocallyConstant = { default := { toFun := Function.const X default, isLocallyConstant := (_ : IsLocallyConstant (Function.const X default)) } }

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

Equations

• LocallyConstant.instFunLikeLocallyConstant = { coe := LocallyConstant.toFun, coe_injective' := (_ : ∀ ⦃a₁ a₂ : LocallyConstant X Y⦄, a₁.toFun = a₂.toFun → a₁ = a₂) }

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].

Equations

• LocallyConstant.Simps.apply f = ⇑f

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

Equations

• ↑f = ContinuousMap.mk ⇑f

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

Equations

• LocallyConstant.instCoeLocallyConstantContinuousMap = { coe := LocallyConstant.toContinuousMap }

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

Equations

• LocallyConstant.const X y = { toFun := Function.const X y, isLocallyConstant := (_ : IsLocallyConstant (Function.const X 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.ofIsClopen {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.

Equations

• LocallyConstant.ofIsClopen hU = { toFun := fun (x : X) => if x ∈ U then 0 else 1, isLocallyConstant := (_ : IsLocallyConstant fun (x : X) => if x ∈ U then 0 else 1) }

@[simp]

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

@[simp]

theorem LocallyConstant.ofIsClopen_fiber_one {X : Type u_5} [TopologicalSpace X] {U : Set X} [(x : X) → Decidable (x ∈ U)] (hU : IsClopen U) : ⇑(LocallyConstant.ofIsClopen 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 : 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.

Equations

• LocallyConstant.map f g = { toFun := f ∘ ⇑g, isLocallyConstant := (_ : IsLocallyConstant (f ∘ g.toFun)) }

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

Equations

• LocallyConstant.flip f a = LocallyConstant.map (fun (f : α → β) => f a) f

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 α.

Equations

• LocallyConstant.unflip f = { toFun := fun (x : X) (a : α) => (f a) x, isLocallyConstant := (_ : IsLocallyConstant fun (x : X) (a : α) => (f a) x) }

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

Equations

• One or more equations did not get rendered due to their size.

@[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 Y Z) => 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.

Equations

• LocallyConstant.desc f h cond inj = { toFun := f, isLocallyConstant := (_ : IsLocallyConstant f) }

@[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, LocallyConstant.indicator returns the locally constant function that is f on U and 0 otherwise.

Equations

• LocallyConstant.indicator f hU = { toFun := Set.indicator U ⇑f, isLocallyConstant := (_ : ∀ (s : Set R), IsOpen (Set.indicator U ⇑f ⁻¹' s)) }

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

Equations

• LocallyConstant.mulIndicator f hU = { toFun := Set.mulIndicator U ⇑f, isLocallyConstant := (_ : ∀ (s : Set R), IsOpen (Set.mulIndicator U ⇑f ⁻¹' s)) }

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

Equations

• One or more equations did not get rendered due to their size.

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₂), f { val := x, property := (_ : x ∈ C₁) } = g { val := x, property := (_ : x ∈ C₂) }) [DecidablePred fun (x : X) => x ∈ 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.

TODO: Generalise this construction to ContinuousMap.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocallyConstant.piecewise_apply_left {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₂), f { val := x, property := (_ : x ∈ C₁) } = g { val := x, property := (_ : x ∈ C₂) }) [DecidablePred fun (x : X) => x ∈ C₁] (x : X) (hx : x ∈ C₁) : (LocallyConstant.piecewise h₁ h₂ h f g hfg) x = f { val := x, property := hx }

@[simp]

theorem LocallyConstant.piecewise_apply_right {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₂), f { val := x, property := (_ : x ∈ C₁) } = g { val := x, property := (_ : x ∈ C₂) }) [DecidablePred fun (x : X) => x ∈ C₁] (x : X) (hx : x ∈ C₂) : (LocallyConstant.piecewise h₁ h₂ h f g hfg) x = g { val := x, property := hx }

noncomputable def LocallyConstant.piecewise' {X : Type u_1} {Z : Type u_3} [TopologicalSpace X] {C₀ : Set X} {C₁ : Set X} {C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁) (h₂ : IsClosed C₂) (f₁ : LocallyConstant (↑C₁) Z) (f₂ : LocallyConstant (↑C₂) Z) [DecidablePred fun (x : X) => x ∈ C₁] (hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ { val := x, property := (_ : x ∈ C₁) } = f₂ { val := x, property := (_ : x ∈ C₂) }) : LocallyConstant (↑C₀) Z

A variant of LocallyConstant.piecewise where the two closed sets cover a subset.

TODO: Generalise this construction to ContinuousMap.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocallyConstant.piecewise'_apply_left {X : Type u_1} {Z : Type u_3} [TopologicalSpace X] {C₀ : Set X} {C₁ : Set X} {C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁) (h₂ : IsClosed C₂) (f₁ : LocallyConstant (↑C₁) Z) (f₂ : LocallyConstant (↑C₂) Z) [DecidablePred fun (x : X) => x ∈ C₁] (hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ { val := x, property := (_ : x ∈ C₁) } = f₂ { val := x, property := (_ : x ∈ C₂) }) (x : ↑C₀) (hx : ↑x ∈ C₁) : (LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ { val := ↑x, property := hx }

@[simp]

theorem LocallyConstant.piecewise'_apply_right {X : Type u_1} {Z : Type u_3} [TopologicalSpace X] {C₀ : Set X} {C₁ : Set X} {C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁) (h₂ : IsClosed C₂) (f₁ : LocallyConstant (↑C₁) Z) (f₂ : LocallyConstant (↑C₂) Z) [DecidablePred fun (x : X) => x ∈ C₁] (hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ { val := x, property := (_ : x ∈ C₁) } = f₂ { val := x, property := (_ : x ∈ C₂) }) (x : ↑C₀) (hx : ↑x ∈ C₂) : (LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ { val := ↑x, property := hx }