TopologicalSemiring.continuousNeg_of_mul
theorem TopologicalSemiring.continuousNeg_of_mul :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : NonAssocRing α] [inst_2 : ContinuousMul α],
ContinuousNeg α
The theorem `TopologicalSemiring.continuousNeg_of_mul` states that for any type `α`, if `α` is equipped with a topology (i.e., is a topological space), is a non-associative ring, and has a continuous multiplication operation, then the negation operation on `α` is continuous. The continuity of negation operation follows from the fact that it is just multiplication with `-1`.
More concisely: If `α` is a topological space, a non-associative ring equipped with a continuous multiplication, then the negation operation on `α` is a continuous function.
|
TopologicalSemiring.toTopologicalRing
theorem TopologicalSemiring.toTopologicalRing :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : NonAssocRing α], TopologicalSemiring α → TopologicalRing α
The theorem `TopologicalSemiring.toTopologicalRing` states that if `R`, represented by the generic type `α`, is a ring and has a topological semiring structure, then it also has a topological ring structure. The existence of this theorem allows us to assign a topological ring structure to `R` without the need to explicitly prove the continuity of the negation operation (`continuous_neg`). In other words, this theorem bridges the gap between topological semirings and topological rings.
More concisely: If a topological semiring is a ring, then it is a topological ring.
|
mulRight_continuous
theorem mulRight_continuous :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : NonUnitalNonAssocRing α] [inst_2 : TopologicalRing α]
(x : α), Continuous ⇑(AddMonoidHom.mulRight x)
This theorem states that in any topological semiring, the right-multiplication operation, represented here as an `AddMonoidHom` (an additive monoid homomorphism), is a continuous function. This means that for every element `x` in the semiring, which is also a topological space, the function that multiplies any given element by `x` on the right is a continuous function with respect to the topology of the semiring.
More concisely: In any topological semiring, the right multiplication operation is a continuous AddMonoidHom (additive monoid homomorphism).
|
mulLeft_continuous
theorem mulLeft_continuous :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : NonUnitalNonAssocRing α] [inst_2 : TopologicalRing α]
(x : α), Continuous ⇑(AddMonoidHom.mulLeft x)
This theorem states that in a topological semiring (a mathematical structure that combines the properties of a semiring and a topological space), the left-multiplication operation, which maps an element to an additive monoid homomorphism that multiplies every input by that element, is a continuous function. In other words, for a given element 'x' in a topological semiring 'α', applying the left-multiplication operation that multiplies by 'x' is a continuous function with respect to the topology on 'α'. Here, the continuity of functions is defined in the sense of topological spaces.
More concisely: In a topological semiring, left-multiplication by an element is a continuous function.
|
TopologicalRing.of_addGroup_of_nhds_zero
theorem TopologicalRing.of_addGroup_of_nhds_zero :
∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalAddGroup R],
Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (nhds 0 ×ˢ nhds 0) (nhds 0) →
(∀ (x₀ : R), Filter.Tendsto (fun x => x₀ * x) (nhds 0) (nhds 0)) →
(∀ (x₀ : R), Filter.Tendsto (fun x => x * x₀) (nhds 0) (nhds 0)) → TopologicalRing R
This theorem states that for any type `R` which has a structure of a non-unital, non-associative ring, a topological space, and a topological additive group, if three conditions are met, `R` is a topological ring. The conditions are as follows:
1. The function that takes two arguments from `R` and multiplies them, when viewed as a function on `R × R`, is continuous at `(0,0)`. In other words, for every neighborhood of 0 in `R`, the preimage of this neighborhood under this multiplication function contains a neighborhood of `(0,0)` in `R × R`.
2. For every element `x₀` of `R`, the function that multiplies `x₀` by its argument is continuous at `0`.
3. For every element `x₀` of `R`, the function that multiplies its argument by `x₀` is continuous at `0`.
In this specific context, continuity at `0` means that for every neighborhood of `0` in `R`, the preimage of this neighborhood under the function contains a neighborhood of `0`.
More concisely: If `R` is a non-unital, non-associative ring endowed with a topology making it a topological space and a topological additive group, such that the multiplication function is continuous at `(0,0)` and the functions `x₀ × _` and `_ × x₀` are continuous at `0` for each `x₀ ∈ R`, then `R` is a topological ring.
|