ContinuousStar.continuous_star
theorem ContinuousStar.continuous_star :
∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Star R] [self : ContinuousStar R], Continuous star := by
sorry
This theorem states that the `star` operator is continuous. In more detail, for any type `R` that is equipped with a topology (i.e., is a topological space), a `star` operation (typically used in the context of complex conjugation or other forms of involution), and a condition that this `star` operation is continuous (`ContinuousStar R`), the `star` operation is indeed continuous. In other words, the image of a continuous function under the `star` operation is also continuous.
More concisely: For any topological space (R, top) equipped with a continuous star operation, the star function is a continuous function.
|
Continuous.star
theorem Continuous.star :
∀ {α : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [inst_2 : ContinuousStar R]
[inst_3 : TopologicalSpace α] {f : α → R}, Continuous f → Continuous fun x => star (f x)
This theorem states that for any types `α` and `R`, where `R` is a topological space, a "star" type (an operation which takes an element and returns its "star" element), and has a continuous "star" operation, and `α` is also a topological space, if `f` is a continuous function from `α` to `R`, then the function that takes `x` in `α` and maps it to the "star" of `f(x)` in `R` is also continuous.
More concisely: If `α` and `R` are topological spaces, `f` is a continuous function from `α` to `R`, and `α` has a continuous star operation, then the function that maps `x` in `α` to the star of `f(x)` in `R` is continuous.
|