Complex.interior_preimage_re
theorem Complex.interior_preimage_re : ∀ (s : Set ℝ), interior (Complex.re ⁻¹' s) = Complex.re ⁻¹' interior s := by
sorry
This theorem states that for any set `s` of real numbers, the interior of the preimage of `s` under the function `Complex.re` (which takes a complex number and returns its real part) is equal to the preimage of the interior of `s` under the same function. In other words, when we take a set of real numbers, get the corresponding set of complex numbers through the real part function, and find the largest open subset of that, it's the same as if we first found the largest open subset of the original set of real numbers and then got the corresponding set of complex numbers. This theorem is about the relationship between the interior operation in topology and the function that gets the real part of a complex number.
More concisely: The interior of the preimage of a real set under the real part function is equal to the preimage of the interior of that set.
|
Complex.isHomeomorphicTrivialFiberBundle_re
theorem Complex.isHomeomorphicTrivialFiberBundle_re : IsHomeomorphicTrivialFiberBundle ℝ Complex.re
The theorem `Complex.isHomeomorphicTrivialFiberBundle_re` asserts that the function `Complex.re`, which takes a complex number and returns its real part, effectively converts the complex numbers (`ℂ`) into a trivial topological fiber bundle over the real numbers (`ℝ`). In other words, there exists a homeomorphism between the complex numbers and the product space of the reals with some fiber, such that this homeomorphism when projected onto the first component of the product space (the reals) gives back the function `Complex.re`.
More concisely: The function `Complex.re` from the complex numbers to the real numbers induces a homeomorphism between the complex numbers and the product space of the real numbers with a trivial fiber, making the complex numbers a trivial topological fiber bundle over the real numbers.
|
Complex.frontier_preimage_re
theorem Complex.frontier_preimage_re : ∀ (s : Set ℝ), frontier (Complex.re ⁻¹' s) = Complex.re ⁻¹' frontier s := by
sorry
This theorem states that for any set `s` of real numbers, the frontier (the set of points between the closure and interior of the set) of the preimage under the real part function of `s` is equal to the preimage under the real part function of the frontier of `s`. In simpler terms, taking the frontier before or after applying the real part function to a set of real numbers does not change the result.
More concisely: The frontier of the real part function applied to a set of real numbers is equal to the real part function applied to the frontier of that set.
|
Complex.isOpenMap_im
theorem Complex.isOpenMap_im : IsOpenMap Complex.im
The theorem `Complex.isOpenMap_im` states that the function that maps a complex number to its imaginary part, `Complex.im`, is an open map. In other words, if we take any open set of complex numbers, the set of their imaginary parts is also an open set in the real numbers.
More concisely: The function `Complex.im` maps open sets of complex numbers to open sets in the real numbers.
|
Complex.frontier_preimage_im
theorem Complex.frontier_preimage_im : ∀ (s : Set ℝ), frontier (Complex.im ⁻¹' s) = Complex.im ⁻¹' frontier s := by
sorry
This theorem states that for any set `s` of real numbers, the frontier (boundary) of the preimage of `s` under the imaginary part function of complex numbers is equal to the preimage of the frontier of `s` under the same function. In other words, when mapping from the complex plane to the real line via the imaginary part function, the boundary of the set of preimages is the same as the set of preimages of the boundaries.
More concisely: The imaginary part function maps the boundary of a set of complex numbers to the boundary of its image, that is, the frontier of the preimage is equal to the preimage of the frontier.
|
Complex.interior_preimage_im
theorem Complex.interior_preimage_im : ∀ (s : Set ℝ), interior (Complex.im ⁻¹' s) = Complex.im ⁻¹' interior s := by
sorry
This theorem states that for any set `s` of real numbers, the interior of the preimage of `s` under the imaginary part function of complex numbers is equal to the preimage of the interior of `s` under the same function. That is, taking the interior of the set of complex numbers whose imaginary part is in `s` gives the same result as taking the set of complex numbers whose imaginary part is in the interior of `s`. The preimage of a set under a function consists of all elements which map into the set under the function. The interior of a set is the largest open set contained within the set, in the context of a topological space.
More concisely: The interior of the preimage of a real set under the imaginary part function of complex numbers is equal to the preimage of the interior of that set.
|
Complex.closure_preimage_im
theorem Complex.closure_preimage_im : ∀ (s : Set ℝ), closure (Complex.im ⁻¹' s) = Complex.im ⁻¹' closure s
The theorem `Complex.closure_preimage_im` states that for any set `s` of real numbers, the closure of the preimage of `s` under the imaginary part function of complex numbers is equal to the preimage of the closure of `s` under the same function. In other words, closing the set before applying the preimage operation with the imaginary part of complex numbers is the same as applying the preimage operation first and then closing the set. This theorem provides a property of continuity for the imaginary part function in the context of topological spaces.
More concisely: The closure of the preimage of a real set under the imaginary part function of complex numbers is equal to the preimage of the closure of that set.
|
Complex.isOpenMap_re
theorem Complex.isOpenMap_re : IsOpenMap Complex.re
This theorem states that the real part function, denoted as `Complex.re`, which maps a complex number to its real part, is an "open map". In the context of topology, an open map is a function between two topological spaces that maps open sets to open sets. Specifically, for any open set of complex numbers, the set of their real parts is an open set of real numbers.
More concisely: The real part function from the complex numbers to the real numbers is a continuous open mapping.
|
Complex.isHomeomorphicTrivialFiberBundle_im
theorem Complex.isHomeomorphicTrivialFiberBundle_im : IsHomeomorphicTrivialFiberBundle ℝ Complex.im
The theorem `Complex.isHomeomorphicTrivialFiberBundle_im` states that the function `Complex.im`, which returns the imaginary part of a complex number, forms a trivial topological fiber bundle over the real numbers `ℝ`. In other words, the space of complex numbers `ℂ` can be projected onto the real numbers `ℝ` by the `Complex.im` function in a way that is homeomorphic (topologically equivalent) to the product space `ℝ × ℝ`. The fibers in this bundle are the inverse images of the `Complex.im` function, and each fiber is topologically equivalent to `ℝ`.
More concisely: The complex numbers' imaginary part function `Complex.im` induces a topologically trivial fiber bundle structure over the real numbers with each fiber being homeomorphic to the real line.
|