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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[[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] |
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: