NonarchimedeanGroup.nonarchimedean_of_emb
theorem NonarchimedeanGroup.nonarchimedean_of_emb :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : NonarchimedeanGroup G] {H : Type u_2}
[inst_3 : Group H] [inst_4 : TopologicalSpace H] [inst_5 : TopologicalGroup H] (f : G →* H),
OpenEmbedding ⇑f → NonarchimedeanGroup H
This theorem states that if there exists an open embedding from a topological group `G` to another group `H`, and if `G` is a nonarchimedean group, then `H` must also be a nonarchimedean group. In other words, the nonarchimedean property is preserved under open embeddings in the context of topological groups.
More concisely: If `G` is an open subgroup of a topological group `H` and `G` is a nonarchimedean topological group, then `H` is also a nonarchimedean topological group.
|
NonarchimedeanGroup.prod_subset
theorem NonarchimedeanGroup.prod_subset :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : NonarchimedeanGroup G] {K : Type u_3}
[inst_3 : Group K] [inst_4 : TopologicalSpace K] [inst_5 : NonarchimedeanGroup K] {U : Set (G × K)},
U ∈ nhds 1 → ∃ V W, ↑V ×ˢ ↑W ⊆ U
This theorem, named `NonarchimedeanGroup.prod_subset`, states that for any two nonarchimedean groups `G` and `K` (which are both groups and topological spaces), given an open neighborhood of the identity in the cartesian product of `G` and `K`, there exist open neighborhoods `V` in `G` and `W` in `K` such that the cartesian product of `V` and `W` is a subset of the original neighborhood. In simpler terms, in nonarchimedean groups, any open neighborhood of the identity in the product space contains a product of open neighborhoods from each group.
More concisely: For any nonarchimedean groups G and K, and any open neighborhood U of the identity in G × K, there exist open neighborhoods V in G and W in K such that V × W ⊆ U.
|
NonarchimedeanRing.left_mul_subset
theorem NonarchimedeanRing.left_mul_subset :
∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : NonarchimedeanRing R]
(U : OpenAddSubgroup R) (r : R), ∃ V, r • ↑V ⊆ ↑U
This theorem, named `NonarchimedeanRing.left_mul_subset`, states that for any nonarchimedean ring `R` equipped with a topological structure, given an open additive subgroup `U` of the ring and any element `r` of the ring, there exists an open additive subgroup `V` such that when every element of `V` is scaled by `r`, the result lies within `U`. This is a property of nonarchimedean rings which can be seen as "local" in the sense that the condition is about what happens near any given element of the ring.
More concisely: For any nonarchimedean ring `R` with topological structure, given an open additive subgroup `U` and an element `r` in `R`, there exists an open additive subgroup `V` such that `r * x ∈ U` for all `x ∈ V`.
|
NonarchimedeanGroup.prod_self_subset
theorem NonarchimedeanGroup.prod_self_subset :
∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : NonarchimedeanGroup G] {U : Set (G × G)},
U ∈ nhds 1 → ∃ V, ↑V ×ˢ ↑V ⊆ U
In the context of nonarchimedean groups, this theorem states that for every open neighborhood of the identity element in the Cartesian square of a nonarchimedean group, there exists an open neighborhood in the group itself such that the Cartesian square of this group neighborhood is contained in the original neighborhood. Here, an open neighborhood of an element in a topological space is a set containing an open set that includes that element, and the Cartesian square of a set is the set of all possible ordered pairs of its elements.
More concisely: In the context of nonarchimedean groups, for every open neighborhood of the identity in the group's Cartesian square, there exists an open neighborhood of the identity such that its Cartesian square is contained in the original neighborhood.
|
NonarchimedeanAddGroup.prod_self_subset
theorem NonarchimedeanAddGroup.prod_self_subset :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : NonarchimedeanAddGroup G]
{U : Set (G × G)}, U ∈ nhds 0 → ∃ V, ↑V ×ˢ ↑V ⊆ U
The theorem `NonarchimedeanAddGroup.prod_self_subset` states that for any nonarchimedean additive group `G` equipped with a topological space structure, if `U` is an open neighborhood (as defined in the topological sense) of the identity in the Cartesian square of `G`, then there exists an open neighborhood `V` of the identity in `G` such that the Cartesian square of `V` is a subset of `U`. In the context of this theorem, a nonarchimedean group is a particular type of group that satisfies certain topological properties, and the Cartesian square of a set is the set of all possible ordered pairs of its elements.
More concisely: For any nonarchimedean additive group `G` with a topological structure, there exists an open neighborhood `V` of the identity in `G` such that the Cartesian square of `V` is contained in any open neighborhood `U` of the identity in the square of `G`.
|
NonarchimedeanAddGroup.prod_subset
theorem NonarchimedeanAddGroup.prod_subset :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : NonarchimedeanAddGroup G]
{K : Type u_3} [inst_3 : AddGroup K] [inst_4 : TopologicalSpace K] [inst_5 : NonarchimedeanAddGroup K]
{U : Set (G × K)}, U ∈ nhds 0 → ∃ V W, ↑V ×ˢ ↑W ⊆ U
This theorem states that for any open neighborhood of the identity in the Cartesian product of two nonarchimedean groups, there exists an open neighborhood in each group such that the Cartesian product of these two open neighborhoods is a subset of the original neighborhood. More formally, given two nonarchimedean groups `G` and `K` with associated topological spaces and a set `U` that is a neighborhood of the identity in the Cartesian product of these groups, there exists sets `V` and `W` which are neighborhoods in `G` and `K` respectively, such that the Cartesian product of `V` and `W` (denoted by `↑V ×ˢ ↑W`) is contained within `U`.
More concisely: Given two nonarchimedean groups `G` and `K` and a neighborhood `U` of the identity in their product, there exist neighborhoods `V` in `G` and `W` in `K` such that `↑V ×ˢ ↑W` is contained in `U`.
|
NonarchimedeanRing.mul_subset
theorem NonarchimedeanRing.mul_subset :
∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : NonarchimedeanRing R]
(U : OpenAddSubgroup R), ∃ V, ↑V * ↑V ⊆ ↑U
This theorem is about a nonarchimedean ring, which is a type of ring in mathematics with specific properties. It states that for every open subgroup `U` of this ring, there exists another open subgroup `V` such that the set of all products of elements from `V` with itself is contained within `U`. This idea is typically expressed in mathematical notation as `∀ U, ∃ V, V * V ⊆ U`. This theorem plays a role in the study of nonarchimedean geometry, a branch of number theory.
More concisely: For every open subgroup `U` of a nonarchimedean ring, there exists an open subgroup `V` such that `V * V` is contained in `U`.
|