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