ContinuityOn Question

Stream: new members

[Dominic Steinitz]

I am trying to prove

import Mathlib

noncomputable
def f : (Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) × EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1)
  | (x, α) =>if (x.val 1) > 0 then α else -α

def s : Set ((Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) × EuclideanSpace ℝ (Fin 1)) := { x | 0 < x.1.val 1 }

example : ContinuousOn f s := by
  have h0 : IsOpen s := sorry
  have h2 : ContinuousOn f s ↔ ∀ (t : Set  (EuclideanSpace ℝ (Fin 1))), IsOpen t → IsOpen (s ∩ f ⁻¹' t) := continuousOn_open_iff h0
  have h3 : ∀ (t : Set  (EuclideanSpace ℝ (Fin 1))), IsOpen t → IsOpen (s ∩ f ⁻¹' t) := sorry
  exact h2.mpr h3

But I seem to be creating many lines of lean to do so. One of the problems I think I have is that I have x.val and x.1.val 1.

Is there a simple way to do this?

[Aaron Liu]

Have you considered using docs#Circle or docs#AddCircle

[Dominic Steinitz]

Yes

[Dominic Steinitz]

I have simplified my problem and have made a bit of progress

noncomputable
def g : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1)
  | (x, α) => if (x 1) > 0 then α else -α

def t : Set (EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 1)) := { x | 0 < x.1 1 }

example : ContinuousOn g t := by
  have h0 : IsOpen t := by
    let pi : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 1) → ℝ := λ p => p.1 1
    have h_cont : Continuous pi := (Continuous.comp (continuous_apply 1) continuous_fst)
    exact isOpen_lt continuous_const h_cont
  sorry

[Aaron Liu]

You can define f like this:

noncomputable
def f (x : (Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) × EuclideanSpace ℝ (Fin 1)) :
    EuclideanSpace ℝ (Fin 1) :=
  if (x.fst.val 1) > 0 then x.snd else -x.snd

[Aaron Liu]

Dominic Steinitz said:

I have simplified my problem and have made a bit of progress

noncomputable
def g : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1)
  | (x, α) => if (x 1) > 0 then α else -α

def t : Set (EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 1)) := { x | 0 < x.1 1 }

example : ContinuousOn g t := by
  have h0 : IsOpen t := by
    let pi : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 1) → ℝ := λ p => p.1 1
    have h_cont : Continuous pi := (Continuous.comp (continuous_apply 1) continuous_fst)
    exact isOpen_lt continuous_const h_cont
  sorry

Here's a simple solution:

example : ContinuousOn g t := by
  apply continuous_snd.continuousOn.congr
  intro x hx
  dsimp [g, t] at hx ⊢
  rw [if_pos hx]

[Dominic Steinitz]

Great - thanks very much - so succinct it seems almost magical - now all I have to do is understand how it does what it does