PolygonalArcEndpointDiskCappedTaperModel
ProvedPolygonalArcEndpointDiskCappedTaperModelA positive-radius, positive-slope endpoint disk-capped taper has open upper and lower regions, each connected and disjoint, while the centerline lies in the taper and removing it splits the taper into those two regions.
Preamble
import Mathlib.Analysis.Convex.PathConnected import Mathlib.Analysis.InnerProductSpace.PiL2 open Set
Formal statement
lemma PolygonalArcEndpointDiskCappedTaperModel (a K : ℝ) (ha : 0 < a) (hK : 0 < K) :
let C : Set (EuclideanSpace ℝ (Fin 2)) :=
{z | 0 < z 0 ∧ z 0 ^ 2 + z 1 ^ 2 < a ^ 2 ∧ -K * z 0 < z 1 ∧ z 1 < K * z 0}
let L : Set (EuclideanSpace ℝ (Fin 2)) :=
{z | 0 < z 0 ∧ z 0 ^ 2 + z 1 ^ 2 < a ^ 2 ∧ 0 < z 1 ∧ z 1 < K * z 0}
let R : Set (EuclideanSpace ℝ (Fin 2)) :=
{z | 0 < z 0 ∧ z 0 ^ 2 + z 1 ^ 2 < a ^ 2 ∧ -K * z 0 < z 1 ∧ z 1 < 0}
let G : Set (EuclideanSpace ℝ (Fin 2)) :=
{z | 0 < z 0 ∧ z 0 < a ∧ z 1 = 0}
IsOpen C ∧ IsOpen L ∧ IsOpen R ∧
IsConnected L ∧ IsConnected R ∧
Disjoint L R ∧ (0 : EuclideanSpace ℝ (Fin 2)) ∉ C ∧
G ⊆ C ∧ C \ G = L ∪ R := by sorrySource