Mathlib.Topology.Piecewise

continuousWithinAt_update_same theorem

[DecidableEq α] {y : β} : ContinuousWithinAt (update f x y) s x ↔ Tendsto f (𝓝[s \ { x }] x) (𝓝 y)

Full source

@[simp]
theorem continuousWithinAt_update_same [DecidableEq α] {y : β} :
    ContinuousWithinAtContinuousWithinAt (update f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y) :=
  calc
    ContinuousWithinAt (update f x y) s x ↔ Tendsto (update f x y) (𝓝[s \ {x}] x) (𝓝 y) := by
    { rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self] }
    _ ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y) :=
      tendsto_congr' <| eventually_nhdsWithin_iff.2 <| Eventually.of_forall
        fun _ hz => update_of_ne hz.2 ..

Continuity of Function Update at Point vs Limit Behavior in Punctured Neighborhood

Informal description

Let $\alpha$ and $\beta$ be topological spaces, $f : \alpha \to \beta$ a function, $s \subseteq \alpha$ a subset, and $x \in \alpha$ a point. Then the updated function $\text{update } f \, x \, y$ is continuous at $x$ within $s$ if and only if $f$ tends to $y$ as the argument approaches $x$ within $s \setminus \{x\}$.

continuousAt_update_same theorem

[DecidableEq α] {y : β} : ContinuousAt (Function.update f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)

Full source

@[simp]
theorem continuousAt_update_same [DecidableEq α] {y : β} :
    ContinuousAtContinuousAt (Function.update f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y) := by
  rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_diff]

Continuity of Function Update at Point vs Limit Behavior in Punctured Neighborhood

Informal description

Let $\alpha$ and $\beta$ be topological spaces, $f \colon \alpha \to \beta$ a function, and $x \in \alpha$ a point. Then the updated function $\text{update } f \, x \, y$ is continuous at $x$ if and only if $f$ tends to $y$ as the argument approaches $x$ within the punctured neighborhood of $x$ (i.e., $\alpha \setminus \{x\}$).

ContinuousOn.if' theorem

 {s : Set α} {p : α → Prop} {f g : α → β} [∀ a, Decidable (p a)]
  (hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 <| if p a then f a else g a))
  (hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 <| if p a then f a else g a))
  (hf : ContinuousOn f <| s ∩ {a | p a}) (hg : ContinuousOn g <| s ∩ {a | ¬p a}) :
  ContinuousOn (fun a => if p a then f a else g a) s

Full source

theorem ContinuousOn.if' {s : Set α} {p : α → Prop} {f g : α → β} [∀ a, Decidable (p a)]
    (hpf : ∀ a ∈ s ∩ frontier { a | p a },
      Tendsto f (𝓝[s ∩ { a | p a }] a) (𝓝 <| if p a then f a else g a))
    (hpg :
      ∀ a ∈ s ∩ frontier { a | p a },
        Tendsto g (𝓝[s ∩ { a | ¬p a }] a) (𝓝 <| if p a then f a else g a))
    (hf : ContinuousOn f <| s ∩ { a | p a }) (hg : ContinuousOn g <| s ∩ { a | ¬p a }) :
    ContinuousOn (fun a => if p a then f a else g a) s := by
  intro x hx
  by_cases hx' : x ∈ frontier { a | p a }
  · exact (hpf x ⟨hx, hx'⟩).piecewise_nhdsWithin (hpg x ⟨hx, hx'⟩)
  · rw [← inter_univ s, ← union_compl_self { a | p a }, inter_union_distrib_left] at hx ⊢
    rcases hx with hx | hx
    · apply ContinuousWithinAt.union
      · exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)
      · have : x ∉ closure { a | p a }ᶜ := fun h => hx' ⟨subset_closure hx.2, by
          rwa [closure_compl] at h⟩
        exact continuousWithinAt_of_not_mem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2
    · apply ContinuousWithinAt.union
      · have : x ∉ closure { a | p a } := fun h =>
          hx' ⟨h, fun h' : x ∈ interior { a | p a } => hx.2 (interior_subset h')⟩
        exact continuousWithinAt_of_not_mem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2
      · exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)

Continuity of Piecewise-Defined Function with Limit Conditions at Frontier

Informal description

Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, $p : X \to \text{Prop}$ a predicate (with decidable values), and $f, g : X \to Y$ functions. Suppose that: 1. For every point $a$ in $s \cap \text{frontier}\{x \mid p(x)\}$, the limit of $f$ as $x$ approaches $a$ within $s \cap \{x \mid p(x)\}$ equals $\begin{cases} f(a) & \text{if } p(a) \\ g(a) & \text{otherwise} \end{cases}$; 2. For every point $a$ in $s \cap \text{frontier}\{x \mid p(x)\}$, the limit of $g$ as $x$ approaches $a$ within $s \cap \{x \mid \neg p(x)\}$ equals $\begin{cases} f(a) & \text{if } p(a) \\ g(a) & \text{otherwise} \end{cases}$; 3. $f$ is continuous on $s \cap \{x \mid p(x)\}$; 4. $g$ is continuous on $s \cap \{x \mid \neg p(x)\}$. Then the piecewise-defined function $x \mapsto \begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases}$ is continuous on $s$.

ContinuousOn.piecewise' theorem

 [∀ a, Decidable (a ∈ t)] (hpf : ∀ a ∈ s ∩ frontier t, Tendsto f (𝓝[s ∩ t] a) (𝓝 (piecewise t f g a)))
  (hpg : ∀ a ∈ s ∩ frontier t, Tendsto g (𝓝[s ∩ tᶜ] a) (𝓝 (piecewise t f g a))) (hf : ContinuousOn f <| s ∩ t)
  (hg : ContinuousOn g <| s ∩ tᶜ) : ContinuousOn (piecewise t f g) s

Full source

theorem ContinuousOn.piecewise' [∀ a, Decidable (a ∈ t)]
    (hpf : ∀ a ∈ s ∩ frontier t, Tendsto f (𝓝[s ∩ t] a) (𝓝 (piecewise t f g a)))
    (hpg : ∀ a ∈ s ∩ frontier t, Tendsto g (𝓝[s ∩ tᶜ] a) (𝓝 (piecewise t f g a)))
    (hf : ContinuousOn f <| s ∩ t) (hg : ContinuousOn g <| s ∩ tᶜ) :
    ContinuousOn (piecewise t f g) s :=
  hf.if' hpf hpg hg

Continuity of Piecewise Function with Limit Conditions at Frontier

Informal description

Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, $t \subseteq X$ a subset with decidable membership, and $f, g : X \to Y$ functions. Suppose that: 1. For every point $a$ in $s \cap \text{frontier}(t)$, the limit of $f$ as $x$ approaches $a$ within $s \cap t$ equals the piecewise value $\begin{cases} f(a) & \text{if } a \in t \\ g(a) & \text{otherwise} \end{cases}$; 2. For every point $a$ in $s \cap \text{frontier}(t)$, the limit of $g$ as $x$ approaches $a$ within $s \cap t^c$ equals the piecewise value $\begin{cases} f(a) & \text{if } a \in t \\ g(a) & \text{otherwise} \end{cases}$; 3. $f$ is continuous on $s \cap t$; 4. $g$ is continuous on $s \cap t^c$. Then the piecewise-defined function $x \mapsto \begin{cases} f(x) & \text{if } x \in t \\ g(x) & \text{otherwise} \end{cases}$ is continuous on $s$.

ContinuousOn.if theorem

 {p : α → Prop} [∀ a, Decidable (p a)] (hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a)
  (hf : ContinuousOn f <| s ∩ closure {a | p a}) (hg : ContinuousOn g <| s ∩ closure {a | ¬p a}) :
  ContinuousOn (fun a => if p a then f a else g a) s

Full source

theorem ContinuousOn.if {p : α → Prop} [∀ a, Decidable (p a)]
    (hp : ∀ a ∈ s ∩ frontier { a | p a }, f a = g a)
    (hf : ContinuousOn f <| s ∩ closure { a | p a })
    (hg : ContinuousOn g <| s ∩ closure { a | ¬p a }) :
    ContinuousOn (fun a => if p a then f a else g a) s := by
  apply ContinuousOn.if'
  · rintro a ha
    simp only [← hp a ha, ite_self]
    apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
    exact hf a ⟨ha.1, ha.2.1⟩
  · rintro a ha
    simp only [hp a ha, ite_self]
    apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
    rcases ha with ⟨has, ⟨_, ha⟩⟩
    rw [← mem_compl_iff, ← closure_compl] at ha
    apply hg a ⟨has, ha⟩
  · exact hf.mono (inter_subset_inter_right s subset_closure)
  · exact hg.mono (inter_subset_inter_right s subset_closure)

Continuity of Piecewise-Defined Function with Matching Boundary Values

Informal description

Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, and $p : X \to \text{Prop}$ a decidable predicate. Given two functions $f, g : X \to Y$ such that: 1. For every point $a$ in $s \cap \text{frontier}\{x \mid p(x)\}$, we have $f(a) = g(a)$; 2. $f$ is continuous on $s \cap \overline{\{x \mid p(x)\}}$; 3. $g$ is continuous on $s \cap \overline{\{x \mid \neg p(x)\}}$. Then the piecewise-defined function $x \mapsto \begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases}$ is continuous on $s$.

ContinuousOn.piecewise theorem

 [∀ a, Decidable (a ∈ t)] (ht : ∀ a ∈ s ∩ frontier t, f a = g a) (hf : ContinuousOn f <| s ∩ closure t)
  (hg : ContinuousOn g <| s ∩ closure tᶜ) : ContinuousOn (piecewise t f g) s

Full source

theorem ContinuousOn.piecewise [∀ a, Decidable (a ∈ t)]
    (ht : ∀ a ∈ s ∩ frontier t, f a = g a) (hf : ContinuousOn f <| s ∩ closure t)
    (hg : ContinuousOn g <| s ∩ closure tᶜ) : ContinuousOn (piecewise t f g) s :=
  hf.if ht hg

Continuity of Piecewise Function with Matching Boundary Values on Closure

Informal description

Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, and $t \subseteq X$ a subset with decidable membership. Given two functions $f, g : X \to Y$ such that: 1. For every point $a$ in $s \cap \text{frontier}(t)$, we have $f(a) = g(a)$; 2. $f$ is continuous on $s \cap \overline{t}$; 3. $g$ is continuous on $s \cap \overline{t^c}$. Then the piecewise-defined function $x \mapsto \begin{cases} f(x) & \text{if } x \in t \\ g(x) & \text{otherwise} \end{cases}$ is continuous on $s$.

continuous_if' theorem

 {p : α → Prop} [∀ a, Decidable (p a)]
  (hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 <| ite (p a) (f a) (g a)))
  (hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 <| ite (p a) (f a) (g a)))
  (hf : ContinuousOn f {x | p x}) (hg : ContinuousOn g {x | ¬p x}) : Continuous fun a => ite (p a) (f a) (g a)

Full source

theorem continuous_if' {p : α → Prop} [∀ a, Decidable (p a)]
    (hpf : ∀ a ∈ frontier { x | p x }, Tendsto f (𝓝[{ x | p x }] a) (𝓝 <| ite (p a) (f a) (g a)))
    (hpg : ∀ a ∈ frontier { x | p x }, Tendsto g (𝓝[{ x | ¬p x }] a) (𝓝 <| ite (p a) (f a) (g a)))
    (hf : ContinuousOn f { x | p x }) (hg : ContinuousOn g { x | ¬p x }) :
    Continuous fun a => ite (p a) (f a) (g a) := by
  rw [continuous_iff_continuousOn_univ]
  apply ContinuousOn.if' <;> simp [*] <;> assumption

Continuity of Piecewise-Defined Function with Limit Conditions at Frontier

Informal description

Let $X$ and $Y$ be topological spaces, $p : X \to \text{Prop}$ a decidable predicate, and $f, g : X \to Y$ functions. Suppose that: 1. For every point $a$ in the frontier of $\{x \mid p(x)\}$, the limit of $f$ as $x$ approaches $a$ within $\{x \mid p(x)\}$ equals $\begin{cases} f(a) & \text{if } p(a) \\ g(a) & \text{otherwise} \end{cases}$; 2. For every point $a$ in the frontier of $\{x \mid p(x)\}$, the limit of $g$ as $x$ approaches $a$ within $\{x \mid \neg p(x)\}$ equals $\begin{cases} f(a) & \text{if } p(a) \\ g(a) & \text{otherwise} \end{cases}$; 3. $f$ is continuous on $\{x \mid p(x)\}$; 4. $g$ is continuous on $\{x \mid \neg p(x)\}$. Then the piecewise-defined function $x \mapsto \begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases}$ is continuous on $X$.

continuous_if theorem

 {p : α → Prop} [∀ a, Decidable (p a)] (hp : ∀ a ∈ frontier {x | p x}, f a = g a)
  (hf : ContinuousOn f (closure {x | p x})) (hg : ContinuousOn g (closure {x | ¬p x})) :
  Continuous fun a => if p a then f a else g a

Full source

theorem continuous_if {p : α → Prop} [∀ a, Decidable (p a)]
    (hp : ∀ a ∈ frontier { x | p x }, f a = g a) (hf : ContinuousOn f (closure { x | p x }))
    (hg : ContinuousOn g (closure { x | ¬p x })) :
    Continuous fun a => if p a then f a else g a := by
  rw [continuous_iff_continuousOn_univ]
  apply ContinuousOn.if <;> simpa

Continuity of Piecewise-Defined Function with Matching Boundary Conditions

Informal description

Let $X$ and $Y$ be topological spaces, and let $p : X \to \text{Prop}$ be a decidable predicate. Given two functions $f, g : X \to Y$ such that: 1. For every point $a$ in the frontier of $\{x \mid p(x)\}$, we have $f(a) = g(a)$; 2. $f$ is continuous on the closure of $\{x \mid p(x)\}$; 3. $g$ is continuous on the closure of $\{x \mid \neg p(x)\}$. Then the piecewise-defined function $x \mapsto \begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases}$ is continuous on $X$.

Continuous.if theorem

 {p : α → Prop} [∀ a, Decidable (p a)] (hp : ∀ a ∈ frontier {x | p x}, f a = g a) (hf : Continuous f)
  (hg : Continuous g) : Continuous fun a => if p a then f a else g a

Full source

theorem Continuous.if {p : α → Prop} [∀ a, Decidable (p a)]
    (hp : ∀ a ∈ frontier { x | p x }, f a = g a) (hf : Continuous f) (hg : Continuous g) :
    Continuous fun a => if p a then f a else g a :=
  continuous_if hp hf.continuousOn hg.continuousOn

Continuity of Piecewise Function with Matching Boundary Conditions

Informal description

Let $X$ and $Y$ be topological spaces, and let $p : X \to \text{Prop}$ be a decidable predicate. Given two continuous functions $f, g : X \to Y$ such that for every point $a$ in the frontier of $\{x \mid p(x)\}$, we have $f(a) = g(a)$, then the piecewise-defined function \[ x \mapsto \begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases} \] is continuous on $X$.

continuous_if_const theorem

 (p : Prop) [Decidable p] (hf : p → Continuous f) (hg : ¬p → Continuous g) : Continuous fun a => if p then f a else g a

Full source

theorem continuous_if_const (p : Prop) [Decidable p] (hf : p → Continuous f)
    (hg : ¬p → Continuous g) : Continuous fun a => if p then f a else g a := by
  split_ifs with h
  exacts [hf h, hg h]

Continuity of a Conditional Function with Constant Condition

Informal description

Let $p$ be a decidable proposition. If $f$ is continuous whenever $p$ holds and $g$ is continuous whenever $\neg p$ holds, then the piecewise function defined by $x \mapsto \begin{cases} f(x) & \text{if } p \\ g(x) & \text{otherwise} \end{cases}$ is continuous.

Continuous.if_const theorem

(p : Prop) [Decidable p] (hf : Continuous f) (hg : Continuous g) : Continuous fun a => if p then f a else g a

Full source

theorem Continuous.if_const (p : Prop) [Decidable p] (hf : Continuous f)
    (hg : Continuous g) : Continuous fun a => if p then f a else g a :=
  continuous_if_const p (fun _ => hf) fun _ => hg

Continuity of Piecewise Function with Constant Condition

Informal description

Let $p$ be a decidable proposition. If $f$ and $g$ are continuous functions, then the piecewise function defined by $x \mapsto \begin{cases} f(x) & \text{if } p \\ g(x) & \text{otherwise} \end{cases}$ is continuous.

continuous_piecewise theorem

 [∀ a, Decidable (a ∈ s)] (hs : ∀ a ∈ frontier s, f a = g a) (hf : ContinuousOn f (closure s))
  (hg : ContinuousOn g (closure sᶜ)) : Continuous (piecewise s f g)

Full source

theorem continuous_piecewise [∀ a, Decidable (a ∈ s)]
    (hs : ∀ a ∈ frontier s, f a = g a) (hf : ContinuousOn f (closure s))
    (hg : ContinuousOn g (closure sᶜ)) : Continuous (piecewise s f g) :=
  continuous_if hs hf hg

Continuity of Piecewise Function with Matching Boundary Conditions

Informal description

Let $X$ and $Y$ be topological spaces, and let $s \subseteq X$ be a set with decidable membership. Given two functions $f, g : X \to Y$ such that: 1. For every point $a$ in the frontier of $s$, we have $f(a) = g(a)$; 2. $f$ is continuous on the closure of $s$; 3. $g$ is continuous on the closure of the complement $s^c$. Then the piecewise-defined function \[ x \mapsto \begin{cases} f(x) & \text{if } x \in s, \\ g(x) & \text{otherwise} \end{cases} \] is continuous on $X$.

Continuous.piecewise theorem

 [∀ a, Decidable (a ∈ s)] (hs : ∀ a ∈ frontier s, f a = g a) (hf : Continuous f) (hg : Continuous g) :
  Continuous (piecewise s f g)

Full source

theorem Continuous.piecewise [∀ a, Decidable (a ∈ s)]
    (hs : ∀ a ∈ frontier s, f a = g a) (hf : Continuous f) (hg : Continuous g) :
    Continuous (piecewise s f g) :=
  hf.if hs hg

Continuity of Piecewise Function with Matching Boundary Conditions

Informal description

Let $X$ and $Y$ be topological spaces, and let $s \subseteq X$ be a set with decidable membership. Given two continuous functions $f, g : X \to Y$ such that $f(a) = g(a)$ for every point $a$ in the frontier of $s$, then the piecewise-defined function \[ x \mapsto \begin{cases} f(x) & \text{if } x \in s, \\ g(x) & \text{otherwise} \end{cases} \] is continuous on $X$.

IsOpen.ite' theorem

(hs : IsOpen s) (hs' : IsOpen s') (ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s') : IsOpen (t.ite s s')

Full source

theorem IsOpen.ite' (hs : IsOpen s) (hs' : IsOpen s')
    (ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s') : IsOpen (t.ite s s') := by
  classical
    simp only [isOpen_iff_continuous_mem, Set.ite] at *
    convert
      continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2
    rename_i x
    by_cases hx : x ∈ t <;> simp [hx]

Openness of If-Then-Else Set with Matching Frontier Conditions

Informal description

Let $X$ be a topological space and $s, s', t \subseteq X$ be subsets. If: 1. $s$ and $s'$ are open sets; 2. For every point $x$ in the frontier of $t$, we have $x \in s$ if and only if $x \in s'$; then the set defined by \[ \text{ite}(t, s, s') := (s \cap t) \cup (s' \cap t^c) \] is open in $X$.

IsOpen.ite theorem

(hs : IsOpen s) (hs' : IsOpen s') (ht : s ∩ frontier t = s' ∩ frontier t) : IsOpen (t.ite s s')

Full source

theorem IsOpen.ite (hs : IsOpen s) (hs' : IsOpen s')
    (ht : s ∩ frontier t = s' ∩ frontier t) : IsOpen (t.ite s s') :=
  hs.ite' hs' fun x hx => by simpa [hx] using Set.ext_iff.1 ht x

Openness of If-Then-Else Set with Matching Frontier Intersections

Informal description

Let $X$ be a topological space and $s, s', t \subseteq X$ be subsets. If: 1. $s$ and $s'$ are open sets; 2. The intersections $s \cap \text{frontier}(t)$ and $s' \cap \text{frontier}(t)$ are equal; then the set defined by \[ \text{ite}(t, s, s') := (s \cap t) \cup (s' \cap t^c) \] is open in $X$.

ite_inter_closure_eq_of_inter_frontier_eq theorem

(ht : s ∩ frontier t = s' ∩ frontier t) : t.ite s s' ∩ closure t = s ∩ closure t

Full source

theorem ite_inter_closure_eq_of_inter_frontier_eq
    (ht : s ∩ frontier t = s' ∩ frontier t) : t.ite s s' ∩ closure t = s ∩ closure t := by
  rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left,
    ite_inter_self, ite_inter_of_inter_eq _ ht]

Intersection of If-Then-Else Set with Closure: $\text{ite}(t, s, s') \cap \overline{t} = s \cap \overline{t}$ when $s \cap \text{frontier}(t) = s' \cap \text{frontier}(t)$

Informal description

For any sets $s, s', t$ in a topological space, if $s \cap \text{frontier}(t) = s' \cap \text{frontier}(t)$, then the intersection of the if-then-else set $\text{ite}(t, s, s')$ with the closure of $t$ equals the intersection of $s$ with the closure of $t$, i.e., $$ \text{ite}(t, s, s') \cap \overline{t} = s \cap \overline{t}. $$

ite_inter_closure_compl_eq_of_inter_frontier_eq theorem

(ht : s ∩ frontier t = s' ∩ frontier t) : t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ

Full source

theorem ite_inter_closure_compl_eq_of_inter_frontier_eq
    (ht : s ∩ frontier t = s' ∩ frontier t) : t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ := by
  rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq]
  rwa [frontier_compl, eq_comm]

Intersection of If-Then-Else Set with Closure of Complement: $\text{ite}(t, s, s') \cap \overline{t^c} = s' \cap \overline{t^c}$ when $s \cap \text{frontier}(t) = s' \cap \text{frontier}(t)$

Informal description

For any sets $s, s', t$ in a topological space, if $s \cap \text{frontier}(t) = s' \cap \text{frontier}(t)$, then the intersection of the if-then-else set $\text{ite}(t, s, s')$ with the closure of the complement of $t$ equals the intersection of $s'$ with the closure of the complement of $t$, i.e., $$ \text{ite}(t, s, s') \cap \overline{t^c} = s' \cap \overline{t^c}. $$

continuousOn_piecewise_ite' theorem

 [∀ x, Decidable (x ∈ t)] (h : ContinuousOn f (s ∩ closure t)) (h' : ContinuousOn g (s' ∩ closure tᶜ))
  (H : s ∩ frontier t = s' ∩ frontier t) (Heq : EqOn f g (s ∩ frontier t)) : ContinuousOn (t.piecewise f g) (t.ite s s')

Full source

theorem continuousOn_piecewise_ite' [∀ x, Decidable (x ∈ t)]
    (h : ContinuousOn f (s ∩ closure t)) (h' : ContinuousOn g (s' ∩ closure tᶜ))
    (H : s ∩ frontier t = s' ∩ frontier t) (Heq : EqOn f g (s ∩ frontier t)) :
    ContinuousOn (t.piecewise f g) (t.ite s s') := by
  apply ContinuousOn.piecewise
  · rwa [ite_inter_of_inter_eq _ H]
  · rwa [ite_inter_closure_eq_of_inter_frontier_eq H]
  · rwa [ite_inter_closure_compl_eq_of_inter_frontier_eq H]

Continuity of Piecewise Function on If-Then-Else Set with Matching Boundary Conditions

Informal description

Let $X$ and $Y$ be topological spaces, $s, s' \subseteq X$ subsets, and $t \subseteq X$ a subset with decidable membership. Given two functions $f, g : X \to Y$ such that: 1. $f$ is continuous on $s \cap \overline{t}$; 2. $g$ is continuous on $s' \cap \overline{t^c}$; 3. $s \cap \text{frontier}(t) = s' \cap \text{frontier}(t)$; 4. $f$ and $g$ agree on $s \cap \text{frontier}(t)$. Then the piecewise-defined function $x \mapsto \begin{cases} f(x) & \text{if } x \in t \\ g(x) & \text{otherwise} \end{cases}$ is continuous on the set $\text{ite}(t, s, s') = (s \cap t) \cup (s' \setminus t)$.

continuousOn_piecewise_ite theorem

 [∀ x, Decidable (x ∈ t)] (h : ContinuousOn f s) (h' : ContinuousOn g s') (H : s ∩ frontier t = s' ∩ frontier t)
  (Heq : EqOn f g (s ∩ frontier t)) : ContinuousOn (t.piecewise f g) (t.ite s s')

Full source

theorem continuousOn_piecewise_ite [∀ x, Decidable (x ∈ t)]
    (h : ContinuousOn f s) (h' : ContinuousOn g s') (H : s ∩ frontier t = s' ∩ frontier t)
    (Heq : EqOn f g (s ∩ frontier t)) : ContinuousOn (t.piecewise f g) (t.ite s s') :=
  continuousOn_piecewise_ite' (h.mono inter_subset_left) (h'.mono inter_subset_left) H Heq

Continuity of Piecewise Function on If-Then-Else Set with Matching Boundary Conditions

Informal description

Let $X$ and $Y$ be topological spaces, $s, s' \subseteq X$ subsets, and $t \subseteq X$ a subset with decidable membership. Given two functions $f, g : X \to Y$ such that: 1. $f$ is continuous on $s$; 2. $g$ is continuous on $s'$; 3. $s \cap \text{frontier}(t) = s' \cap \text{frontier}(t)$; 4. $f$ and $g$ agree on $s \cap \text{frontier}(t)$. Then the piecewise-defined function $x \mapsto \begin{cases} f(x) & \text{if } x \in t \\ g(x) & \text{otherwise} \end{cases}$ is continuous on the set $\text{ite}(t, s, s') = (s \cap t) \cup (s' \setminus t)$.