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|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 (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