Complex.starConvex_ofReal_slitPlane
theorem Complex.starConvex_ofReal_slitPlane : ∀ {x : ℝ}, 0 < x → StarConvex ℝ (↑x) Complex.slitPlane
The theorem `Complex.starConvex_ofReal_slitPlane` states that the slit plane in complex numbers, which is the complex plane with the closed negative real axis removed, is star-shaped at any positive real number. In more detail, for any positive real number `x`, every line segment from `x` to any point in the slit plane is completely contained within the slit plane. This is a property of star-convex sets, where the line segment connecting any two points within the set also resides within the set.
More concisely: For any positive real number x, the slit complex plane (excluding the closed negative real axis) is star-shaped around x, meaning every line segment from x to any point in the slit plane lies entirely within the slit plane.
|
Complex.starConvex_slitPlane
theorem Complex.starConvex_slitPlane : ∀ {z : ℂ}, 0 < z → StarConvex ℝ z Complex.slitPlane
This theorem states that the slit plane (which is the complex plane with the closed negative real axis removed) is star-convex at any positive number. In other words, for any positive complex number `z`, every line segment that starts at `z` and ends at any point in the slit plane is entirely contained within the slit plane.
More concisely: For any positive complex number `z`, every line segment between `z` and a point in the complex plane with the closed negative real axis removed lies entirely in the same half-plane as `z`.
|
Complex.convexHull_reProdIm
theorem Complex.convexHull_reProdIm : ∀ (s t : Set ℝ), (convexHull ℝ) (s ×ℂ t) = (convexHull ℝ) s ×ℂ (convexHull ℝ) t
The theorem `Complex.convexHull_reProdIm` states that for any two sets of real numbers `s` and `t`, the convex hull of the Cartesian product of `s` and `t` in the complex numbers (denoted as `s ×ℂ t`) is the same as the Cartesian product of the convex hull of `s` and the convex hull of `t` in the complex numbers. In other words, taking the convex hull of the complex Cartesian product of two sets is the same as first taking the convex hulls of the individual sets and then taking their complex Cartesian product.
More concisely: The convex hull of a Cartesian product of sets in the complex numbers is equal to the Cartesian product of their convex hulls in the complex numbers.
|
Complex.starConvex_one_slitPlane
theorem Complex.starConvex_one_slitPlane : StarConvex ℝ 1 Complex.slitPlane
The theorem `Complex.starConvex_one_slitPlane` states that the slit plane, which is the set of all complex numbers either with a positive real part or a non-zero imaginary part, is star-convex at `1`. In more detail, this means that for any complex number in the slit plane, any point on the line segment that connects this point and `1` (inclusive) is also in the slit plane. Essentially, you can "travel" from `1` to any other point in the slit plane without leaving the slit plane itself. The line segment is defined by a convex combination (a weighted average where weights sum up to 1 and are non-negative) of `1` and the other point.
More concisely: The slit plane, consisting of complex numbers with positive real part or non-zero imaginary part, is star-convex at 1, meaning any point on the line segment between 1 and any complex number in the slit plane lies within the slit plane.
|