Large finite point sets have four collinear points or a visible six-clique
Lax56.MainTheorem · concepts/Lax56/MainTheorem.lean · lax-56
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Every finite set of at least points in the real plane contains four distinct collinear points or six distinct points that pairwise see one another with respect to the whole set.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax56.Geometry |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Large finite point sets have four collinear points or a visible six-clique |
| 6 | type: theorem |
| 7 | --- |
| 8 | Every finite set of at least `10^(2^450)` points in the real plane contains |
| 9 | four distinct collinear points or six distinct points that pairwise see one |
| 10 | another with respect to the whole set. |
| 11 | -/ |
| 12 | |
| 13 | namespace Lax56.MainTheorem |
| 14 | |
| 15 | open Lax56.Geometry |
| 16 | |
| 17 | axiom large_point_set_four_collinear_or_visible_six |
| 18 | (P : Finset Point) (hP : 10 ^ (2 ^ 450) ≤ P.card) : |
| 19 | HasFourCollinear P ∨ HasVisibleClique P 6 |
| 20 | |
| 21 | end Lax56.MainTheorem |
| 22 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments