UpperHalfPlane.ext'
theorem UpperHalfPlane.ext' : ∀ {a b : UpperHalfPlane}, a.re = b.re → a.im = b.im → a = b
This theorem, referred to as the Extensionality Lemma, states that for any two points 'a' and 'b' in the Upper Half Plane, if the real part (re) of point 'a' equals the real part of point 'b' and the imaginary part (im) of point 'a' equals the imaginary part of point 'b', then point 'a' and point 'b' are the same point. In other words, each point in the Upper Half Plane is uniquely defined by its real and imaginary parts.
More concisely: In the Upper Half Plane, two complex numbers are equal if and only if their real parts are equal and their imaginary parts are equal.
|
UpperHalfPlane.normSq_pos
theorem UpperHalfPlane.normSq_pos : ∀ (z : UpperHalfPlane), 0 < Complex.normSq ↑z
The theorem `UpperHalfPlane.normSq_pos` states that for any point `z` in the open upper half plane, the norm squared of `z` is strictly positive. Here, the open upper half plane is defined as the set of complex numbers with a strictly positive imaginary part, while the complex norm squared is the sum of the square of the real part and the square of the imaginary part of a complex number. Hence, the theorem is essentially asserting a property about the magnitude of points in the open upper half plane in the complex plane.
More concisely: The norm squared of every complex number in the open upper half plane is strictly positive.
|
UpperHalfPlane.im_pos
theorem UpperHalfPlane.im_pos : ∀ (z : UpperHalfPlane), 0 < z.im
This theorem states that for any point `z` in the open upper half plane, the imaginary part of `z`, as given by the function `UpperHalfPlane.im`, is always greater than zero. In other words, the imaginary part of any point in the upper half plane is always positive.
More concisely: For any point in the open upper half plane, its imaginary part is positive.
|