How to define functions from or to intervals.

Stream: new members

[Mattia Bottoni]

Hi everybody :)

I want to prove statements like this in Lean 4:
Show that \R and (√2, +∞) have equal cardinality by describing a bijection from one to the other. Describe your bijection with a formula.

I already know how to show that a function is injective and surjective, but I don’t know how to define a function from \R to (√2, +∞) in Lean.
Is that possible? I want to use the function f(x) = √2 + e^x.

Thank you all in advance!

[Eric Wieser]

You can use ℝ → Set.Ioi (Real.sqrt 2) as the type of the function

[Eric Wieser]

(docs#Set.Ioi)

[Ruben Van de Velde]

Alternatively, write something like

import Mathlib

noncomputable def f (x : ℝ) : ℝ := Real.sqrt 2 + Real.exp x

example : Set.MapsTo f Set.univ (Set.Ioi <| Real.sqrt 2) := by
  sorry

[Ruben Van de Velde]

Or more to the point,

import Mathlib

noncomputable def f (x : ℝ) : ℝ := Real.sqrt 2 + Real.exp x

example : Set.BijOn f Set.univ (Set.Ioi <| Real.sqrt 2) := by
  sorry

[Ruben Van de Velde]

Is this missing from mathlib?

theorem C (g : ℝ  → ℝ) (s) (h : Set.SurjOn g s (Set.Ioi 0)) (a) : Set.SurjOn (a + g ·) s (Set.Ioi a) := by
  intro x hx
  have : x - a ∈ Set.Ioi 0 := by
    simpa using hx
  simpa [eq_sub_iff_add_eq'] using h this

(can be generalized, presumably)

[Yaël Dillies]

This is basically just composition with a bijective function. But it's not in mathlib verbatim.

[Ruben Van de Velde]

Thanks for the pointer; the other function doesn't even need to be bijective (or surjective):

theorem C (g : ℝ  → ℝ) (s) (h : Set.SurjOn g s (Set.Ioi 0)) (a) : Set.SurjOn (a + g ·) s (Set.Ioi a) := by
  simpa using h.comp_left (a + ·)

[Ruben Van de Velde]

I'm also surprised we don't seem to have

theorem C : Set.SurjOn g Set.univ (Set.range g) := by
  intro x
  simp only [Set.image_univ, imp_self]

[Yaël Dillies]

It's a corollary of docs#Set.surjOn_image

[Ruben Van de Velde]

Thanks again, Yaëlsearch :)

[Mattia Bottoni]

Thank you all for your efforts :)