I hereby claim:
- I am smaug123 on github.
- I am patrickstevens (https://keybase.io/patrickstevens) on keybase.
- I have a public key ASAXpP1UQX-aNITZNR8uGTEIh64umJJxGQAAQcoPBIY-bQo
To claim this, I am signing this object:
-- https://math.stackexchange.com/a/4894379/259262 | |
import Mathlib.Data.Real.Sqrt | |
import Mathlib.Tactic.Hint | |
import Mathlib.Tactic.Cases | |
import Mathlib.Algebra.Order.Floor | |
open Real Set | |
namespace Problem |
module Range where | |
-- Preliminaries | |
record True : Set where | |
data False : Set where | |
data _≡_ {A : Set} (x : A) : A → Set where | |
refl : x ≡ x | |
{-# BUILTIN EQUALITY _≡_ #-} | |
data _||_ (A : Set) (B : Set) : Set where |
I hereby claim:
To claim this, I am signing this object: