Polygonal disks in a half-plane

The bordered Radó step approximates the one-skeleton inside the closed right half-plane. This file records the elementary but important consequence: once the replacement polygon stays in that half-plane, its bounded Schoenflies filling stays there as well.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.convex_halfPlaneSet : Convex ℝ HalfPlaneSet

The model closed half-plane is convex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegion_subset_halfPlane (J : PolygonalCircle) (hcarrier : J.carrier ⊆ HalfPlaneSet) : J.closedRegion ⊆ HalfPlaneSet

A polygonal circle carried by the closed right half-plane bounds its disk there.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.coordZero_pos_of_mem_open_subset_halfPlane {O : Set Plane} (hO : IsOpen O) (hOH : O ⊆ HalfPlaneSet) {x : Plane} (hx : x ∈ O) : 0 < x.ofLp 0

A plane-open subset of the closed half-plane cannot contain a point of its supporting boundary line.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mem_carrier_of_mem_closedRegion_coordZero (J : PolygonalCircle) (hcarrier : J.carrier ⊆ HalfPlaneSet) {x : Plane} (hx : x ∈ J.closedRegion) (hxZero : x.ofLp 0 = 0) : x ∈ J.carrier

The supporting line meets the filled polygonal disk only on its polygonal boundary.