Documentation

Mathlib.Topology.LocallyConstant.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 IsLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : XY) :

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

Equations
Instances For
    theorem IsLocallyConstant.tfae {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : XY) :
    [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].TFAE
    theorem IsLocallyConstant.isOpen_fiber {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : XY} (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 : XY} (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 : XY} (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 : XY) :
    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 : XY) :
    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 : XY} (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 : XY} (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 : XY} :
    IsLocallyConstant f ∀ (x : X), IsOpen (f ⁻¹' {f x})
    theorem IsLocallyConstant.iff_isOpen_fiber {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : XY} :
    IsLocallyConstant f ∀ (y : Y), IsOpen (f ⁻¹' {y})
    theorem IsLocallyConstant.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsLocallyConstant f) :
    theorem IsLocallyConstant.iff_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] :
    ∀ {x : TopologicalSpace Y} [inst : DiscreteTopology Y] (f : XY), IsLocallyConstant f Continuous f
    theorem IsLocallyConstant.of_constant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : XY) (h : ∀ (x y : X), f x = f y) :
    theorem IsLocallyConstant.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] {f : XY} (hf : IsLocallyConstant f) (g : YZ) :
    theorem IsLocallyConstant.prod_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Y' : Type u_5} {f : XY} {f' : XY'} (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 : XY₁} {g : XY₂} (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 : YZ} {f : XY} (hg : IsLocallyConstant g) (hf : Continuous f) :
    theorem IsLocallyConstant.apply_eq_of_isPreconnected {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : XY} (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 : XY} (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 : XY} (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 : XY} (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 : XY} :
    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 : XY} (hf : IsLocallyConstant f) :
    (Set.range f).Finite
    theorem IsLocallyConstant.neg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Neg Y] ⦃f : XY (hf : IsLocallyConstant f) :
    theorem IsLocallyConstant.inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Inv Y] ⦃f : XY (hf : IsLocallyConstant f) :
    theorem IsLocallyConstant.add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Add Y] ⦃f : XY ⦃g : XY (hf : IsLocallyConstant f) (hg : IsLocallyConstant g) :
    theorem IsLocallyConstant.mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Mul Y] ⦃f : XY ⦃g : XY (hf : IsLocallyConstant f) (hg : IsLocallyConstant g) :
    theorem IsLocallyConstant.sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Sub Y] ⦃f : XY ⦃g : XY (hf : IsLocallyConstant f) (hg : IsLocallyConstant g) :
    theorem IsLocallyConstant.div {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Div Y] ⦃f : XY ⦃g : XY (hf : IsLocallyConstant f) (hg : IsLocallyConstant 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) :

    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 : XY} (h : ∀ (x y : X), y connectedComponent xf y = f x) :
    theorem IsLocallyConstant.of_constant_on_connected_clopens {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LocallyConnectedSpace X] {f : XY} (h : ∀ (U : Set X), IsConnected UIsClopen UxU, yU, f y = f x) :
    theorem IsLocallyConstant.of_constant_on_preconnected_clopens {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LocallyConnectedSpace X] {f : XY} (h : ∀ (U : Set X), IsPreconnected UIsClopen UxU, yU, f y = f x) :
    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 : XY

      The underlying function.

    • isLocallyConstant : IsLocallyConstant self.toFun

      The map is locally constant.

    Instances For
      theorem LocallyConstant.isLocallyConstant {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] (self : LocallyConstant X Y) :

      The map is locally constant.

      Equations
      • LocallyConstant.instInhabited = { default := { toFun := Function.const X default, isLocallyConstant := } }
      instance LocallyConstant.instFunLike {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] :
      Equations
      • LocallyConstant.instFunLike = { coe := LocallyConstant.toFun, coe_injective' := }
      def LocallyConstant.Simps.apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : LocallyConstant X Y) :
      XY

      See Note [custom simps projections].

      Equations
      Instances For
        @[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 : XY) (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_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

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

        Equations
        • f = { toFun := f, continuous_toFun := }
        Instances For

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

          Equations
          • LocallyConstant.instCoeContinuousMap = { 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) :

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

          Equations
          Instances For
            @[simp]
            theorem LocallyConstant.coe_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (y : Y) :
            def LocallyConstant.ofIsClopen {X : Type u_5} [TopologicalSpace X] {U : Set X} [(x : X) → Decidable (x U)] (hU : IsClopen U) :

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

            Equations
            Instances For
              @[simp]
              theorem LocallyConstant.ofIsClopen_fiber_zero {X : Type u_5} [TopologicalSpace X] {U : Set X} [(x : X) → Decidable (x U)] (hU : IsClopen U) :
              @[simp]
              theorem LocallyConstant.ofIsClopen_fiber_one {X : Type u_5} [TopologicalSpace X] {U : Set X} [(x : X) → Decidable (x U)] (hU : IsClopen 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.range f).Finite
              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) :
              def LocallyConstant.map {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (f : YZ) (g : LocallyConstant X Y) :

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

              Equations
              Instances For
                @[simp]
                theorem LocallyConstant.map_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (f : YZ) (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] :
                @[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₂) :
                def LocallyConstant.flip {X : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace X] (f : LocallyConstant X (αβ)) (a : α) :

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

                Equations
                Instances For
                  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
                  Instances For
                    @[simp]
                    theorem LocallyConstant.unflip_flip {X : Type u_5} {α : Type u_6} {β : Type u_7} [Finite α] [TopologicalSpace X] (f : LocallyConstant X (αβ)) :
                    @[simp]
                    theorem LocallyConstant.flip_unflip {X : Type u_5} {α : Type u_6} {β : Type u_7} [Finite α] [TopologicalSpace X] (f : αLocallyConstant X β) :
                    def LocallyConstant.comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (g : LocallyConstant Y Z) :

                    Pull back of locally constant maps under a continuous map, by pre-composition.

                    Equations
                    Instances For
                      @[simp]
                      theorem LocallyConstant.coe_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (g : LocallyConstant Y Z) :
                      (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 : C(X, Y)) (g : LocallyConstant Y Z) (x : X) :
                      (LocallyConstant.comap f g) x = g (f x)
                      theorem LocallyConstant.comap_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {W : Type u_5} [TopologicalSpace W] (f : C(W, X)) (g : C(X, Y)) (x : LocallyConstant Y Z) :
                      theorem LocallyConstant.comap_const {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (y : Y) (h : ∀ (x : X), f x = y) :
                      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) :

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

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

                        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
                        • f.indicator hU = { toFun := U.indicator f, isLocallyConstant := }
                        Instances For
                          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 (U.indicator 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) :
                          (f.mulIndicator hU) x = U.mulIndicator (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) :
                          (f.indicator hU) x = U.indicator (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) :

                          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
                          • f.mulIndicator hU = { toFun := U.mulIndicator f, isLocallyConstant := }
                          Instances For
                            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) :
                            (f.indicator 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) :
                            (f.mulIndicator 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) :
                            (f.indicator 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) :
                            (f.mulIndicator 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 : aU) :
                            (f.indicator 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 : aU) :
                            (f.mulIndicator hU) a = 1
                            @[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) (g : LocallyConstant Y Z) :
                            (LocallyConstant.congrLeft e).symm g = LocallyConstant.comap e.toContinuousMap g
                            @[simp]
                            theorem LocallyConstant.congrLeft_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (g : LocallyConstant X Z) :
                            (LocallyConstant.congrLeft e) g = LocallyConstant.comap e.symm.toContinuousMap g

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

                            Equations
                            Instances For
                              @[simp]
                              theorem LocallyConstant.congrRight_symm_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (e : Y Z) (g : LocallyConstant X Z) :
                              @[simp]
                              theorem LocallyConstant.congrRight_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (e : Y Z) (g : LocallyConstant X Y) :
                              def LocallyConstant.congrRight {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (e : Y Z) :

                              The equivalence between LocallyConstant X Y and LocallyConstant X Z given an equivalence Y ≃ Z

                              Equations
                              Instances For

                                The set of clopen subsets of a topological space is equivalent to the locally constant maps to a two-element set

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  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 x, = g x, ) [DecidablePred fun (x : X) => x C₁] :

                                  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
                                  • LocallyConstant.piecewise h₁ h₂ h f g hfg = { toFun := fun (i : X) => if hi : i C₁ then f i, hi else g i, , isLocallyConstant := }
                                  Instances For
                                    @[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 x, = g x, ) [DecidablePred fun (x : X) => x C₁] (x : X) (hx : x C₁) :
                                    (LocallyConstant.piecewise h₁ h₂ h f g hfg) x = f x, 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 x, = g x, ) [DecidablePred fun (x : X) => x C₁] (x : X) (hx : x C₂) :
                                    (LocallyConstant.piecewise h₁ h₂ h f g hfg) x = g x, hx
                                    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₁ x, = f₂ x, ) :
                                    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.
                                    Instances For
                                      @[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₁ x, = f₂ x, ) (x : C₀) (hx : x C₁) :
                                      (LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ x, 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₁ x, = f₂ x, ) (x : C₀) (hx : x C₂) :
                                      (LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ x, hx