Erdős Problem 503 #659
Erdős Problem 503 #659
Conversation
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Nice, especially doing all of the statements on the page.
I left a few initial comments, but looks good in general..
| theorem erdos_503 {n : ℕ} : ∃ A : Set (ESpace n), isoscelesSet A ∧ (∀ B : Set (ESpace n), | ||
| isoscelesSet B → B.ncard ≤ A.ncard) ∧ A.ncard = answer(sorry) := by |
There was a problem hiding this comment.
one could use IsGreatest here
also below.
But perhaps even better define the largest such that separately using iSup or sSup then we can use it all over the place?
mo271
added
Erdős Problems
Awaiting author
|
Apologies for the delay! I wasn't sure how to best define "largest such that", so I decided to use |
callesonne
removed
the
Awaiting author
callesonne
left a comment
callesonne
left a comment
There was a problem hiding this comment.
Thanks for the contribution! Here are some comments :)
callesonne
left a comment
callesonne
left a comment
There was a problem hiding this comment.
This is ready to go after my final comment has been adressed, thanks a lot!
Fixed now, and no prob 🙂 |
3 participants
Adds Erdős Problem 503.