Subspace topology and continuous functions

Stream: new members

[Joseph Cooper]

import Mathlib

open Classical

noncomputable
def ex_function: ℝ → ℝ:=
  Set.piecewise ({x|x≤0}) (fun x ↦ 0) (fun x ↦ 1)

example: Continuous ({x | x ≤ 0}.restrict ex_function):= by
  apply continuousOn_iff_continuous_restrict.mp
  apply ContinuousOn.piecewise
  rintro a ⟨l,r⟩
  sorry

I wish to prove that this function is continuous with respect to the subspace topology, when restricted to {x|x≤0}. However, I am left with the goals

a : ℝ
l : a ∈ {x | x ≤ 0}
r : a ∈ frontier {x | x ≤ 0}
⊢ 0 = 1

and the frontier of {x|x ≤ 0} = {0} wrt to the standard topology on ℝ. But I want to use the fact the frontier of {x|x ≤ 0} is empty wrt to the subspace topology. How do I do this?

[Damien Thomine]

I wish to prove that this function is continuous with respect to the subspace topology, when restricted to {x|x≤0}. However, I am left with the goals

I would do things a bit differently. The lemma Set.restrict_piecewise let you simplify the goal at the beginning. Hence, something like

example: Continuous ({x | x ≤ 0}.restrict ex_function):= by
  unfold ex_function
  rw [Set.restrict_piecewise (fun _ ↦ 0) (fun _ ↦ 1) {x | x ≤ 0}]

will do most of the work for you. Since Set.restrict_piecewise is a simp lemma, you can make things shorter (but less explicit) with

example: Continuous ({x | x ≤ 0}.restrict ex_function):= by
  simp [ex_function]