# 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} [] (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} [] (f : XY) :
[, ∀ (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), x U x'U, f x' = f x].TFAE
theorem IsLocallyConstant.of_discrete {X : Type u_1} {Y : Type u_2} [] [] (f : XY) :
theorem IsLocallyConstant.isOpen_fiber {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (y : Y) :
IsOpen {x : X | f x = y}
theorem IsLocallyConstant.isClosed_fiber {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (y : Y) :
IsClosed {x : X | f x = y}
theorem IsLocallyConstant.isClopen_fiber {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (y : Y) :
IsClopen {x : X | f x = y}
theorem IsLocallyConstant.iff_exists_open {X : Type u_1} {Y : Type u_2} [] (f : XY) :
∀ (x : X), ∃ (U : Set X), x U x'U, f x' = f x
theorem IsLocallyConstant.iff_eventually_eq {X : Type u_1} {Y : Type u_2} [] (f : XY) :
∀ (x : X), ∀ᶠ (y : X) in nhds x, f y = f x
theorem IsLocallyConstant.exists_open {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (x : X) :
∃ (U : Set X), x U x'U, f x' = f x
theorem IsLocallyConstant.eventually_eq {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (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} [] {f : XY} :
∀ (x : X), IsOpen (f ⁻¹' {f x})
theorem IsLocallyConstant.iff_isOpen_fiber {X : Type u_1} {Y : Type u_2} [] {f : XY} :
∀ (y : Y), IsOpen (f ⁻¹' {y})
theorem IsLocallyConstant.continuous {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsLocallyConstant.iff_continuous {X : Type u_1} {Y : Type u_2} [] :
∀ {x : } [inst : ] (f : XY),
theorem IsLocallyConstant.of_constant {X : Type u_1} {Y : Type u_2} [] (f : XY) (h : ∀ (x y : X), f x = f y) :
theorem IsLocallyConstant.const {X : Type u_1} {Y : Type u_2} [] (y : Y) :
theorem IsLocallyConstant.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] {f : XY} (hf : ) (g : YZ) :
theorem IsLocallyConstant.prod_mk {X : Type u_1} {Y : Type u_2} [] {Y' : Type u_5} {f : XY} {f' : XY'} (hf : ) (hf' : ) :
IsLocallyConstant fun (x : X) => (f x, f' x)
theorem IsLocallyConstant.comp₂ {X : Type u_1} [] {Y₁ : Type u_5} {Y₂ : Type u_6} {Z : Type u_7} {f : XY₁} {g : XY₂} (hf : ) (hg : ) (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} [] [] {g : YZ} {f : XY} (hg : ) (hf : ) :
theorem IsLocallyConstant.apply_eq_of_isPreconnected {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) {s : Set X} (hs : ) {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} [] {f : XY} (hf : ) (x : X) (y : X) :
f x = f y
theorem IsLocallyConstant.eq_const {X : Type u_1} {Y : Type u_2} [] {f : XY} (hf : ) (x : X) :
f = Function.const X (f x)
theorem IsLocallyConstant.exists_eq_const {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
∃ (y : Y), f =
theorem IsLocallyConstant.iff_is_const {X : Type u_1} {Y : Type u_2} [] {f : XY} :
∀ (x y : X), f x = f y
theorem IsLocallyConstant.range_finite {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
().Finite
theorem IsLocallyConstant.zero {X : Type u_1} {Y : Type u_2} [] [Zero Y] :
theorem IsLocallyConstant.one {X : Type u_1} {Y : Type u_2} [] [One Y] :
theorem IsLocallyConstant.neg {X : Type u_1} {Y : Type u_2} [] [Neg Y] ⦃f : XY (hf : ) :
theorem IsLocallyConstant.inv {X : Type u_1} {Y : Type u_2} [] [Inv Y] ⦃f : XY (hf : ) :
theorem IsLocallyConstant.add {X : Type u_1} {Y : Type u_2} [] [Add Y] ⦃f : XY ⦃g : XY (hf : ) (hg : ) :
theorem IsLocallyConstant.mul {X : Type u_1} {Y : Type u_2} [] [Mul Y] ⦃f : XY ⦃g : XY (hf : ) (hg : ) :
theorem IsLocallyConstant.sub {X : Type u_1} {Y : Type u_2} [] [Sub Y] ⦃f : XY ⦃g : XY (hf : ) (hg : ) :
theorem IsLocallyConstant.div {X : Type u_1} {Y : Type u_2} [] [Div Y] ⦃f : XY ⦃g : XY (hf : ) (hg : ) :
theorem IsLocallyConstant.desc {X : Type u_1} [] {α : Type u_5} {β : Type u_6} (f : Xα) (g : αβ) (h : IsLocallyConstant (g f)) (inj : ) :

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} [] {f : XY} (h : ∀ (x y : X), f y = f x) :
theorem IsLocallyConstant.of_constant_on_connected_clopens {X : Type u_1} {Y : Type u_2} [] {f : XY} (h : ∀ (U : Set X), xU, yU, f y = f x) :
theorem IsLocallyConstant.of_constant_on_preconnected_clopens {X : Type u_1} {Y : Type u_2} [] {f : XY} (h : ∀ (U : Set X), xU, yU, f y = f x) :
structure LocallyConstant (X : Type u_5) (Y : Type u_6) [] :
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} [] (self : ) :

The map is locally constant.

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

See Note [custom simps projections].

Equations
Instances For
@[simp]
theorem LocallyConstant.toFun_eq_coe {X : Type u_1} {Y : Type u_2} [] (f : ) :
f.toFun = f
@[simp]
theorem LocallyConstant.coe_mk {X : Type u_1} {Y : Type u_2} [] (f : XY) (h : ) :
{ toFun := f, isLocallyConstant := h } = f
theorem LocallyConstant.congr_fun {X : Type u_1} {Y : Type u_2} [] {f : } {g : } (h : f = g) (x : X) :
f x = g x
theorem LocallyConstant.congr_arg {X : Type u_1} {Y : Type u_2} [] (f : ) {x : X} {y : X} (h : x = y) :
f x = f y
theorem LocallyConstant.coe_injective {X : Type u_1} {Y : Type u_2} [] :
Function.Injective DFunLike.coe
theorem LocallyConstant.coe_inj {X : Type u_1} {Y : Type u_2} [] {f : } {g : } :
f = g f = g
theorem LocallyConstant.ext {X : Type u_1} {Y : Type u_2} [] ⦃f : ⦃g : (h : ∀ (x : X), f x = g x) :
f = g
theorem LocallyConstant.ext_iff {X : Type u_1} {Y : Type u_2} [] {f : } {g : } :
f = g ∀ (x : X), f x = g x
theorem LocallyConstant.continuous {X : Type u_1} {Y : Type u_2} [] [] (f : ) :
def LocallyConstant.toContinuousMap {X : Type u_1} {Y : Type u_2} [] [] (f : ) :
C(X, Y)

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

Equations
• f = { toFun := f, continuous_toFun := }
Instances For
instance LocallyConstant.instCoeContinuousMap {X : Type u_1} {Y : Type u_2} [] [] :
Coe () C(X, Y)

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} [] [] (f : ) :
f = f
theorem LocallyConstant.toContinuousMap_injective {X : Type u_1} {Y : Type u_2} [] [] :
Function.Injective LocallyConstant.toContinuousMap
def LocallyConstant.const (X : Type u_5) {Y : Type u_6} [] (y : Y) :

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

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

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

Equations
• = { toFun := fun (x : X) => if x U then 0 else 1, isLocallyConstant := }
Instances For
@[simp]
theorem LocallyConstant.ofIsClopen_fiber_zero {X : Type u_5} [] {U : Set X} [(x : X) → Decidable (x U)] (hU : ) :
⁻¹' {0} = U
@[simp]
theorem LocallyConstant.ofIsClopen_fiber_one {X : Type u_5} [] {U : Set X} [(x : X) → Decidable (x U)] (hU : ) :
⁻¹' {1} = U
theorem LocallyConstant.locallyConstant_eq_of_fiber_zero_eq {X : Type u_5} [] (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} [] [] (f : ) :
().Finite
theorem LocallyConstant.apply_eq_of_isPreconnected {X : Type u_1} {Y : Type u_2} [] (f : ) {s : Set X} (hs : ) {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} [] (f : ) (x : X) (y : X) :
f x = f y
theorem LocallyConstant.eq_const {X : Type u_1} {Y : Type u_2} [] (f : ) (x : X) :
theorem LocallyConstant.exists_eq_const {X : Type u_1} {Y : Type u_2} [] [] (f : ) :
∃ (y : Y),
def LocallyConstant.map {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] (f : YZ) (g : ) :

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

Equations
• = { toFun := f g, isLocallyConstant := }
Instances For
@[simp]
theorem LocallyConstant.map_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] (f : YZ) (g : ) :
() = f g
@[simp]
theorem LocallyConstant.map_id {X : Type u_1} {Y : Type u_2} [] :
= id
@[simp]
theorem LocallyConstant.map_comp {X : Type u_1} [] {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} [] (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} [] [] (f : α) :
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
• = { toFun := fun (x : X) (a : α) => (f a) x, isLocallyConstant := }
Instances For
@[simp]
theorem LocallyConstant.unflip_flip {X : Type u_5} {α : Type u_6} {β : Type u_7} [] [] (f : LocallyConstant X (αβ)) :
@[simp]
theorem LocallyConstant.flip_unflip {X : Type u_5} {α : Type u_6} {β : Type u_7} [] [] (f : α) :
.flip = f
def LocallyConstant.comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : C(X, Y)) (g : ) :

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

Equations
• = { toFun := g f, isLocallyConstant := }
Instances For
@[simp]
theorem LocallyConstant.coe_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : C(X, Y)) (g : ) :
() = g f
theorem LocallyConstant.coe_comap_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : C(X, Y)) (g : ) (x : X) :
() x = g (f x)
@[simp]
theorem LocallyConstant.comap_id {X : Type u_1} {Z : Type u_3} [] :
theorem LocallyConstant.comap_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] {W : Type u_5} [] (f : C(W, X)) (g : C(X, Y)) :
theorem LocallyConstant.comap_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] {W : Type u_5} [] (f : C(W, X)) (g : C(X, Y)) (x : ) :
= LocallyConstant.comap (g.comp f) x
theorem LocallyConstant.comap_const {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : C(X, Y)) (y : Y) (h : ∀ (x : X), f x = y) :
= fun (g : ) => LocallyConstant.const X (g y)
theorem LocallyConstant.comap_injective {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (f : C(X, Y)) (hfs : Function.Surjective f.toFun) :
def LocallyConstant.desc {X : Type u_5} {α : Type u_6} {β : Type u_7} [] {g : αβ} (f : Xα) (h : ) (cond : g f = h) (inj : ) :

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} [] (f : Xα) (g : αβ) (h : ) (cond : g f = h) (inj : ) :
(LocallyConstant.desc f h cond inj) = f
noncomputable def LocallyConstant.indicator {X : Type u_1} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) (hU : ) :

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} [] {R : Type u_1} [Zero R] {U : Set X} (f : ) (hU : ) (s : Set R) :
IsOpen (U.indicator f ⁻¹' s)
@[simp]
theorem LocallyConstant.mulIndicator_apply {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) (hU : ) (x : X) :
(f.mulIndicator hU) x = U.mulIndicator (f) x
@[simp]
theorem LocallyConstant.indicator_apply {X : Type u_1} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) (hU : ) (x : X) :
(f.indicator hU) x = U.indicator (f) x
noncomputable def LocallyConstant.mulIndicator {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) (hU : ) :

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} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) (a : X) (hU : ) :
(f.indicator hU) a = if a U then f a else 0
theorem LocallyConstant.mulIndicator_apply_eq_if {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) (a : X) (hU : ) :
(f.mulIndicator hU) a = if a U then f a else 1
theorem LocallyConstant.indicator_of_mem {X : Type u_1} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) {a : X} (hU : ) (h : a U) :
(f.indicator hU) a = f a
theorem LocallyConstant.mulIndicator_of_mem {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) {a : X} (hU : ) (h : a U) :
(f.mulIndicator hU) a = f a
theorem LocallyConstant.indicator_of_not_mem {X : Type u_1} [] {R : Type u_5} [Zero R] {U : Set X} (f : ) {a : X} (hU : ) (h : aU) :
(f.indicator hU) a = 0
theorem LocallyConstant.mulIndicator_of_not_mem {X : Type u_1} [] {R : Type u_5} [One R] {U : Set X} (f : ) {a : X} (hU : ) (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} [] [] (e : X ≃ₜ Y) (g : ) :
.symm g = LocallyConstant.comap e.toContinuousMap g
@[simp]
theorem LocallyConstant.congrLeft_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (e : X ≃ₜ Y) (g : ) :
= LocallyConstant.comap e.symm.toContinuousMap g
def LocallyConstant.congrLeft {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] (e : X ≃ₜ Y) :

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} [] (e : Y Z) (g : ) :
.symm g = LocallyConstant.map (e.symm) g
@[simp]
theorem LocallyConstant.congrRight_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] (e : Y Z) (g : ) :
def LocallyConstant.congrRight {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] (e : Y Z) :

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

Equations
Instances For
def LocallyConstant.equivClopens (X : Type u_1) [] [(s : Set X) → (x : X) → Decidable (x s)] :

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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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