Define convex quadrilateral

Stream: Is there code for X?

[yulia wang]

Hi,everyone. I want to define convex quadrilateral.Can I define it on a two-dimensional plane?

[Kenny Lau]

What do you want to do with it?

[yulia wang]

I want to formalize IMO problems and complete the proofs.

[yulia wang]

The definition of convex quadrilaterals is used in some IMO geometry problems.

[Joseph Myers]

#Proofs from the book > Amsterdam @ 💬 has my suggestions for how API for polygons should be set up. There are lots of different ways you might define convex polygons; obviously the API should include proofs that as many definitions are you can think of are all equivalent to each other. For example, a convex polygon is one with at least three vertices and where for every two consecutive vertices, all others are strictly on the same side of their affine span. Or it's one with at least three vertices and where for every three vertices in the same cyclic order, the obvious determinant (in terms of basis vectors for the two-dimensional affine subspace spanned by the vertices) has the same sign. Or it's one with at least three vertices and where every subset of four vertices in cyclic order is convex.

What's less clear to me is how to define weakly convex polygons (ones that allow repeated vertices and vertices in the middle of edges), without also allowing edges to repeatedly go back and forth along the same line segment which doesn't fit with an intuitive informal notion of weakly convex polygons. But since informal problems with convex polygons are most likely to mean strictly convex, this seems less important.

[Violeta Hernández]

I would argue there are two separate definitions of "polygon" in use in mathematics:

• A cyclically ordered set of points
• A two-dimensional convex polytope

The latter should be relatively straightforward to convert into the former. The opposite conversion is quite more difficult. The Jordan curve theorem tells you that if the polygon is simple (no edges intersect outside of the vertices), then there's a well-defined interior and exterior. A weakly convex polygon is then a polygon (1st definition) whose interior is convex, and a convex polygon is one where moreover every vertex is a vertex of the closure of its interior.

[Violeta Hernández]

Now I suspect this discussion is mostly moot. In my experience solving IMO geometry problems, very few of them actually need any convexity hypotheses. They're mostly just there to avoid mentions of directed angles, or to make the drawings more uniform to the graders' convenience.