TrivSqZeroExt.continuous_fst
theorem TrivSqZeroExt.continuous_fst :
∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M],
Continuous TrivSqZeroExt.fst
This theorem states that for any types `R` and `M`, if `R` and `M` are both topological spaces, then the canonical projection `TrivSqZeroExt.fst`, which maps from `TrivSqZeroExt R M` to `R`, is a continuous function. This means that the preimage of any open set in `R` under the function `TrivSqZeroExt.fst` is also an open set in `TrivSqZeroExt R M`.
More concisely: The canonical projection of the trivial square zero extension of topological spaces `R` and `M`, `TrivSqZeroExt.fst : TrivSqZeroExt R M → R`, is a continuous function.
|
TrivSqZeroExt.topologicalSemiring
theorem TrivSqZeroExt.topologicalSemiring :
∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Semiring R]
[inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module Rᵐᵒᵖ M] [inst_6 : TopologicalSemiring R]
[inst_7 : ContinuousAdd M] [inst_8 : ContinuousSMul R M] [inst_9 : ContinuousSMul Rᵐᵒᵖ M],
TopologicalSemiring (TrivSqZeroExt R M)
The theorem `TrivSqZeroExt.topologicalSemiring` states that for any types `R` and `M`, given the conditions that `R` and `M` are topological spaces, `R` is a semiring, `M` is an additive commutative monoid and a module over `R` and its opposite ring `Rᵐᵒᵖ`, the operations of addition and scalar multiplication on `M` are continuous, and `R` is a topological semiring, then the trivial square-zero extension of `M` over `R`, denoted as `TrivSqZeroExt R M`, forms a topological semiring.
In simpler terms, this means that the set of all pairs `(r, m)` where `r` is in `R` and `m` is in `M`, equipped with a specific multiplication operation, behaves as a topological semiring under certain conditions, preserving both the algebraic structure (semiring) and topological structure when these operations are performed.
More concisely: Given topological spaces `R` (a semiring) and `M` (an additive commutative `R`-module and `Rᵐᵒᵖ`-module with continuous addition and scalar multiplication), the trivial square-zero extension `TrivSqZeroExt R M` forms a topological semiring.
|
TrivSqZeroExt.continuous_snd
theorem TrivSqZeroExt.continuous_snd :
∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M],
Continuous TrivSqZeroExt.snd
The theorem `TrivSqZeroExt.continuous_snd` states that for any two types `R` and `M` - where `R` and `M` have topological space structures - the canonical projection `TrivSqZeroExt.snd`, which maps an element of `TrivSqZeroExt R M` to `M`, is a continuous function. In mathematical terms, this function preserves the topological structure of the space `TrivSqZeroExt R M` when mapping to `M`.
More concisely: The canonical projection `TrivSqZeroExt.snd` from `TrivSqZeroExt R M` to `M` is a continuous function between the topological spaces `TrivSqZeroExt R M` and `M`.
|