I hereby claim:
- I am urkud on github.
- I am urkud (https://keybase.io/urkud) on keybase.
- I have a public key ASCZ1-7hsoJLYycGPz6kEvWquYlbz1jIwtJBdaul1N1Wqwo
To claim this, I am signing this object:
I hereby claim:
To claim this, I am signing this object:
[[a, b, c, d]| let as = filter ((==2) . length . nub . show) [1..360], a <- as, let bs = filter ((==2) . length . nub . (show a ++) . show) as, b <- bs, c <- bs, d <- bs, a + b + c + d == 360] |
Filter | Meaning |
---|---|
at_top |
filter generated by [x, +∞) |
at_bot |
filter generated by (-∞, x] |
𝓝 x |
neighborhoods of x |
𝓝[s] x |
neighborhoods of x within s |
𝓝[Ici x] x |
right neighborhoods of x |
𝓝[Ioi x] x |
punctured right neighborhoods of x |
𝓝[Iio x] x |
punctured left neighborhoods of x |
𝓝[{x}ᶜ] x |
punctured neighborhoods of x |
import Mathlib.Data.Real.NNReal | |
-- Solution of https://www.facebook.com/groups/mathpuz/posts/2449634078545753/ | |
-- formalized in Lean 4 | |
-- depends on https://github.com/leanprover-community/mathlib4 | |
open NNReal Set | |
namespace hidden |