Zulip Chat Archive

Stream: new members

Topic: Subspace topology and continuous functions


Joseph Cooper (Jul 15 2024 at 11:02):

import Mathlib

open Classical

noncomputable
def ex_function:   :=
  Set.piecewise ({x|x0}) (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 (Jul 15 2024 at 16:07):

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]

Last updated: May 02 2025 at 03:31 UTC