Choosing a point from a set

Stream: new members

[Dominic Steinitz]

As an exercise, I have defined a smooth map on manifolds as

def smooth_map (f : M → N) : Prop :=
  ∀ (x : M), Smooth (𝓡 m) (𝓡 n)
    ((chartAt (EuclideanSpace ℝ (Fin n)) (f x)).toFun ∘ f ∘ (chartAt (EuclideanSpace ℝ (Fin m)) x).invFun)

and am trying to prove

theorem smooth_is_continuous {f : M -> N} (hf : smooth_map m n f) : Continuous f := by
sorry

The proof will take any open U in N then since Smooth (in the Mathlib sense) implies Continuous $(\phi \circ f \circ \psi^{-1})^{-1}(\phi(U))$ is open and using the homeo properties of charts and the continuity of functions show that $f^{-1}(U)$ is open.

So now my question: as far as I can see, I can define chartAt (EuclideanSpace ℝ (Fin n)) p but how do I get a p from U? This does not work:

theorem smooth_is_continuous {f : M -> N} (hf : smooth_map m n f) : Continuous f := by
  rw [continuous_def] at *
  intro U hU
  let p := Classical.choice U.Nonempty
  let φ := chartAt (EuclideanSpace ℝ (Fin n)) p
  sorry

[Bjørn Kjos-Hanssen]

Can you post a #mwe please?

[Dominic Steinitz]

I don't have a working example which is why I am asking for help. Here's my full code so far

import Mathlib

open Manifold

variable
  (m : ℕ) {M : Type*}
  [TopologicalSpace M]
  [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
  [SmoothManifoldWithCorners (𝓡 m) M]

variable
  (n : ℕ) {N : Type*}
  [TopologicalSpace N]
  [ChartedSpace (EuclideanSpace ℝ (Fin n)) N]
  [SmoothManifoldWithCorners (𝓡 n) N]

variable
  (p : ℕ) {P : Type*}
  [TopologicalSpace P]
  [ChartedSpace (EuclideanSpace ℝ (Fin p)) P]
  [SmoothManifoldWithCorners (𝓡 p) P]

def smooth_map (f : M → N) : Prop :=
  ∀ (x : M), Smooth (𝓡 m) (𝓡 n)
    ((chartAt (EuclideanSpace ℝ (Fin n)) (f x)).toFun ∘ f ∘ (chartAt (EuclideanSpace ℝ (Fin m)) x).invFun)

theorem smooth_is_continuous {f : M -> N} (hf : smooth_map m n f) : Continuous f := by

  rw [continuous_def] at *
  intro U hU
  let p := Classical.choice U.Nonempty
  let φ := chartAt (EuclideanSpace ℝ (Fin n)) p
  sorry

[Luigi Massacci]

It doesn’t work because as lean is telling you, you don’t know that it is nonempty

[Luigi Massacci]

You can do something like by_cases (hnu : Set.Nonempty U)

[Luigi Massacci]

and then handle the two cases separately

[Michael Rothgang]

Side note: mathlib already has a proof of this fact. It is fine to re-prove things as an exercise, though!