Zulip Chat Archive

Stream: new members

Topic: How to turn an exists_unique into a function?


Kent Van Vels (Jan 20 2025 at 02:58):

I am interested in proving a few simple things about the floor and ceiling functions.

In mathlib there is a function/proof that the floor exists called Real.exists_floor.

I have done straightforward task of showing that this floor is unique and now I want to turn this into a function. What follows is minimal working example.

import Mathlib.Tactic

theorem exists_unique_floor (x : ): ∃! ub : , (ub : )  x   z : , (z : )  x  z  ub := by
  rcases Real.exists_floor x with fl,hfl0,hfl1⟩⟩
  use fl
  apply And.intro
  exact hfl0,hfl1
  intro y hy0,hy1
  apply le_antisymm (hfl1 y hy0) (hy1 fl hfl0)

--noncomputable?
def myFloor (x : ) :  := by
  sorry
  --choose i using Real.exists_floor x doesn't work
  --what do I do here?

Matt Diamond (Jan 20 2025 at 03:03):

Just to be clear, you want to use your own lemma here and not the existing integer Floor function (i.e. docs#Int.floor) in mathlib, right?

Kent Van Vels (Jan 20 2025 at 03:06):

Well... I will use those. But I didn't know about them. :smile:

Even so, I still would like to know if it is possible to turn a "exists_unique" into a function somehow.

Matt Diamond (Jan 20 2025 at 03:09):

Sure... you can write (exists_unique_floor x).choose and mark the function as noncomputable

Matt Diamond (Jan 20 2025 at 03:10):

docs#Exists.choose and docs#Exists.choose_spec are available whenever you want to pick a value from an Exists statement

Kent Van Vels (Jan 20 2025 at 03:11):

Ok. Thank you! I appreciate it and I appreciate the tip on the existing (ha) functions.

Matt Diamond (Jan 20 2025 at 03:13):

no problem!


Last updated: May 02 2025 at 03:31 UTC