AffineMap.lineMap_continuous
theorem AffineMap.lineMap_continuous :
∀ {R : Type u_1} {F : Type u_3} [inst : AddCommGroup F] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalAddGroup F] [inst_3 : Ring R] [inst_4 : Module R F] [inst_5 : TopologicalSpace R]
[inst_6 : ContinuousSMul R F] {p v : F}, Continuous ⇑(AffineMap.lineMap p v)
The theorem `AffineMap.lineMap_continuous` states that for any ring `R`, any additively commutative topological group `F` which is also a module over `R`, and any two points `p` and `v` in `F`, the affine line map from `R` to `F` that sends `0` to `p` and `1` to `v` is a continuous function. This means that the image of any open set under this map is also open, which is a fundamental property in topology and allows for further analytical manipulations using the concept of continuity.
More concisely: For any ring R, additively commutative topological group F as an R-module, and points p, v in F, the affine map from R to F sending 0 to p and 1 to v is a continuous function.
|
AffineMap.continuous_iff
theorem AffineMap.continuous_iff :
∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E]
[inst_2 : AddCommGroup F] [inst_3 : TopologicalSpace F] [inst_4 : TopologicalAddGroup F] [inst_5 : Ring R]
[inst_6 : Module R E] [inst_7 : Module R F] {f : E →ᵃ[R] F}, Continuous ⇑f ↔ Continuous ⇑f.linear
This theorem states that for any affine map `f` from a topological vector space `E` to another topological vector space `F`, both over a ring `R`, the map is continuous if and only if the underlying linear map of `f` is continuous. This theorem is helpful in understanding the relationship and properties between an affine map and its corresponding linear map in terms of continuity.
More concisely: A continuous affine map between topological vector spaces over a ring is equivalent to its underlying linear map being continuous.
|