subset_mul_closure_one
theorem subset_mul_closure_one :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] (s : Set G), s ⊆ s * closure {1}
The theorem `subset_mul_closure_one` states that for any set `s` of a topological group `G`, the set `s` is a subset of the multiplication of `s` and the closure of the set containing only the group's unit element `1`. In other words, every element of `s` can be expressed as the product of an element in `s` and an element in the closure of the set `{1}`. The closure of a set is the smallest closed set containing the set, implying it includes all limit points of the set.
More concisely: For any topological group G and set s of G, every element of s lies in the closure of {1} \* s.
|
exists_closed_nhds_one_inv_eq_mul_subset
theorem exists_closed_nhds_one_inv_eq_mul_subset :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] {U : Set G},
U ∈ nhds 1 → ∃ V ∈ nhds 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U
The theorem `exists_closed_nhds_one_inv_eq_mul_subset` states that for any topological group `G`, if a set `U` is a neighborhood of the identity element `1`, then there exists another neighborhood `V` of the identity which has the following properties: it is closed, it is symmetric (i.e., the inverse of `V` is `V` itself), and the set obtained by multiplying `V` by itself is a subset of `U`.
More concisely: For any topological group G and neighborhood U of the identity 1, there exists a closed and symmetric neighborhood V of 1 such that V ^2 ⊆ U.
|
TopologicalAddGroup.continuous_conj_sum
theorem TopologicalAddGroup.continuous_conj_sum :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : Add G] [inst_3 : ContinuousAdd G]
[inst_4 : ContinuousNeg G], Continuous fun g => g.1 + g.2 + -g.1
The theorem `TopologicalAddGroup.continuous_conj_sum` states that for any type `G` that has a topological space structure, a negation operation, and an addition operation, if both addition and negation are continuous operations, then the conjugation operation, defined as taking a pair of elements (`g.1` and `g.2`) and producing `g.1 + g.2 - g.1`, is also a continuous operation.
More concisely: If `G` is a topological group with continuous negation and addition operations, then the conjugation operation `g => g.1 + g.2 - g.1` is continuous.
|
nhds_translation_add_neg
theorem nhds_translation_add_neg :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G] (x : G),
Filter.comap (fun x_1 => x_1 + -x) (nhds 0) = nhds x
This theorem, `nhds_translation_add_neg`, states that for any type `G` which is a topological space, an additive group, and a topological additive group (these are structures where the group operation is continuous), the filter obtained by taking the preimage under the function `x_1 => x_1 + -x` of the neighborhood filter at `0` is equal to the neighborhood filter at `x`. In other words, if you shift the points of the space by `-x` and look at the neighborhoods around `0`, it's the same as looking at the neighborhoods around `x` in the original space. This theorem demonstrates a sort of "translational symmetry" in topological additive groups.
More concisely: For any topological additive group G, the preimage under x => x + (-x) of the neighborhood filter at 0 is equal to the neighborhood filter at x.
|
eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group
theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : TopologicalSpace α] [inst_4 : Zero α] [inst_5 : T1Space α] {f : G → α} {k : Set G},
IsCompact k → Function.support f ⊆ k → Continuous f → f = 0 ∨ LocallyCompactSpace G
This theorem states that for a function `f` defined on a topological group `G` mapping to a topological space `α` with zero element, if the support of the function (the set of points where the function is nonzero) is contained within a compact set `k`, then either the function is identically zero or the group `G` is locally compact. Here, a topological space is said to be locally compact if every point in it has a compact neighborhood. The theorem also assumes that the function `f` is continuous, and the space `α` has the T1 separation property, meaning that for any two distinct points in `α`, each has a neighborhood not containing the other.
More concisely: If `f` is a continuous function from a topological group `G` to a locally compact, T1 topological space `α` with zero element, and the support of `f` is compact, then either `f` is identically zero or `G` is locally compact.
|
HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group
theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : TopologicalSpace α] [inst_4 : Zero α] [inst_5 : T1Space α] {f : G → α},
HasCompactSupport f → Continuous f → f = 0 ∨ LocallyCompactSpace G
The theorem states that if a function, defined on a topological group, has compact support, then either the function is identically zero or the group is locally compact. This means that for any such function with this property, if the closure of the set where the function is non-zero is compact, it implies that the function has to be either zero everywhere (the trivial function) or the group has the characteristic that every point has a compact neighborhood, termed as being locally compact. This theorem is proven under the assumptions that the group operations are continuous (TopologicalGroup), the function is continuous (Continuous), and every singleton set is closed (T1Space).
More concisely: A continuous function on a topological group with compact support is either the trivial function or the group is locally compact.
|
Filter.Tendsto.inv
theorem Filter.Tendsto.inv :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : ContinuousInv G] {f : α → G}
{l : Filter α} {y : G}, Filter.Tendsto f l (nhds y) → Filter.Tendsto (fun x => (f x)⁻¹) l (nhds y⁻¹)
This theorem states that if a function, within the context of a multiplicative topological group, converges to a certain value, then the inverse of this function converges to the inverse of that value. More formally, given a function `f` from an arbitrary type `α` to a topological space `G`, if `f` tends to a limit `y` (i.e., for every neighborhood of `y`, the pre-image under `f` of this neighborhood is a neighborhood in the domain of `f`) as described by `Filter.Tendsto f l (nhds y)`, then the function that maps `x` to the inverse of `f(x)` also tends to the inverse of `y`. The conditions that `G` is a topological space, has a defined operation of inversion (`Inv G`), and this inversion operation is continuous (`ContinuousInv G`), are also required. Note that this theorem is stated in general for any multiplicative topological group, and there is a specific version applicable for normed fields where the limit is non-zero.
More concisely: If a multiplicative topological group homomorphism `f : α → G` with `G` being a topological space, having a continuous inversion operation, tends to a limit `y` in `G`, then the function that maps each `x` to the inverse of `f(x)` tends to the inverse of `y`.
|
QuotientAddGroup.isOpenMap_coe
theorem QuotientAddGroup.isOpenMap_coe :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
(N : AddSubgroup G), IsOpenMap QuotientAddGroup.mk
The theorem `QuotientAddGroup.isOpenMap_coe` states that for any type `G`, given a topological space structure, an addition group structure, and a topological addition group structure on `G`, along with an addition subgroup `N` of `G`, the canonical map from `G` to the quotient `G ⧸ N`, given by `QuotientAddGroup.mk`, is an open map. This means that the image of any open set in `G` under this map is an open set in the quotient `G ⧸ N`.
More concisely: The map from a group `G` with topological addition group structure to its quotient `G / N` by an additive subgroup `N`, given by `QuotientAddGroup.mk`, is an open map.
|
QuotientGroup.nhds_eq
theorem QuotientGroup.nhds_eq :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] (N : Subgroup G)
(x : G), nhds ↑x = Filter.map QuotientGroup.mk (nhds x)
The theorem `QuotientGroup.nhds_eq` states that for any topological group `G` and subgroup `N` of `G`, and any element `x` in `G`, the neighborhood filter of the quotient `x` in the quotient group `G/N` (represented as `↑x`) is precisely the forward image under the canonical quotient map `QuotientGroup.mk` of the neighborhood filter of `x` in `G`. In other words, neighborhoods in the quotient group are precisely the images of neighborhoods in the original group under the quotient map.
More concisely: The neighborhood filter of a quotient element in a quotient group is equal to the forward image of the neighborhood filter of the element in the original group under the canonical quotient map.
|
map_add_left_nhds
theorem map_add_left_nhds :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G] (x y : G),
Filter.map (fun x_1 => x + x_1) (nhds y) = nhds (x + y)
This theorem states that for any type `G` that is a topological space, an additive group, and a topological additive group, for any elements `x` and `y` of `G`, the forward map of the neighborhood filter at `y` under the addition of `x` is equal to the neighborhood filter at `x + y`. In simpler terms, it says that if we shift each element in a neighborhood of `y` by adding `x`, then the resulting set is a neighborhood of `x + y` in the given topological additive group.
More concisely: For any topological additive group `G` and elements `x, y` in `G`, the forward neighborhood filters at `x` and `x + y` are equal.
|
compact_open_separated_mul_left
theorem compact_open_separated_mul_left :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : MulOneClass G] [inst_2 : ContinuousMul G] {K U : Set G},
IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 1, V * K ⊆ U
This theorem states that, for a given topological space `G` with a multiplication operation and continuous multiplication, if `K` is a compact set within an open set `U`, then there exists an open neighborhood `V` of the multiplicative identity `1` such that the set resulting from multiplying `V` and `K` is a subset of `U`. Here, `IsCompact` denotes compactness of a set in the topological space, `IsOpen` denotes openness of a set in this space, and `nhds 1` denotes the neighborhood filter at `1`. The multiplication `V * K` is assumed to be defined in a way compatibly with the underlying topology and the algebraic structure.
More concisely: Given a topological group `(G, ∓)` with continuous multiplication, if `K` is a compact subset of an open set `U` in `G`, then there exists an open neighborhood `V` of the identity `1` such that `V * K ⊆ U`.
|
TopologicalGroup.continuous_conj
theorem TopologicalGroup.continuous_conj :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : Mul G] [inst_3 : ContinuousMul G] (g : G),
Continuous fun h => g * h * g⁻¹
This theorem states that for any given type `G`, if `G` has a topological space structure, an inverse operation, a multiplication operation, and the multiplication is continuous, then the conjugation by a fixed element `g` is also continuous. Here, the conjugation of an element `h` by `g` is defined as `g * h * g⁻¹`.
More concisely: If `G` is a type equipped with a topological space structure, an inverse operation, and a continuous multiplication, then the conjugation by a fixed element is a continuous map on `G`.
|
continuous_sub_right
theorem continuous_sub_right :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G] (a : G),
Continuous fun x => x - a
This theorem states that for any type `G` that has a topological space structure, a subtraction operation, and for which subtraction is continuous, and for any element `a` of type `G`, the function that subtracts `a` from its argument is a continuous function. In mathematical terms, if you consider a topological space `G` with a defined subtraction operation that is continuous, then for any fixed `a` in `G`, the function `f(x) = x - a` is also continuous.
More concisely: For any topological space `G` equipped with a continuous subtraction operation, the function `x ↔ x - a` is continuous for all `a` in `G`.
|
exists_disjoint_smul_of_isCompact
theorem exists_disjoint_smul_of_isCompact :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : NoncompactSpace G] {K L : Set G}, IsCompact K → IsCompact L → ∃ g, Disjoint K (g • L)
The theorem states that in a noncompact topological group, given any two compact sets, it is possible to find a translation of the second set that does not intersect with the first set. In other words, for every two compact sets K and L in this group, there exists an element g in the group such that the set {g * l | l ∈ L} (the translate of L by g) is disjoint from K. This means that the infimum (greatest lower bound) of any element in both the translated set and K is the bottom element of the lattice structure of the group. This theorem establishes a property about how compact sets can be partitioned in noncompact topological groups.
More concisely: In a noncompact topological group, given any two compact sets, there exists a translation that maps one set to a disjoint subset of the other.
|
Inducing.continuousNeg
theorem Inducing.continuousNeg :
∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] [inst_2 : TopologicalSpace G]
[inst_3 : TopologicalSpace H] [inst_4 : ContinuousNeg H] {f : G → H},
Inducing f → (∀ (x : G), f (-x) = -f x) → ContinuousNeg G
The theorem `Inducing.continuousNeg` states that given two types `G` and `H` with negation operations, and equipped with topological structures, if the negation operation is continuous in `H` and there exists a function `f` from `G` to `H` which is an inducing function (it keeps the topological structure), and this function `f` also preserves the negation operation (i.e. `f` of `-x` equals `-f` of `x` for every `x` in `G`), then the negation operation is also continuous in `G`. This theorem is related to the continuity of the negation operation under certain conditions in the world of topological spaces.
More concisely: If `f` is a continuous, negation-preserving inducing function from a topological space `(G, top_G)` to another topological space `(H, top_H)` with continuous negation operation, then the negation operation is continuous on `(G, top_G)`.
|
IsClosed.smul_left_of_isCompact
theorem IsClosed.smul_left_of_isCompact :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group α]
[inst_3 : MulAction α β] [inst_4 : ContinuousInv α] [inst_5 : ContinuousSMul α β] {s : Set α} {t : Set β},
IsClosed t → IsCompact s → IsClosed (s • t)
The theorem `IsClosed.smul_left_of_isCompact` states that if you have a set `s` of elements of some type `α` in a topological group (where α is equipped with a topological space structure and a group structure, and the group operation is continuous) and a set `t` of another type `β` in a topological space (where β is equipped with a topological space structure and a multiplication action of α on β that is continuous), and if `t` is a closed set and `s` is a compact set, then the scalar multiplication of `s` and `t` (represented by `s • t`) is also a closed set. In other words, the left scalar multiplication of a compact set by a closed set in a topological group under a continuous action is a closed set.
More concisely: If `s` is a compact set in a topological group with continuous group action on a closed set `t`, then the scalar multiplication `s • t` is a closed set.
|
TopologicalAddGroup.exists_antitone_basis_nhds_zero
theorem TopologicalAddGroup.exists_antitone_basis_nhds_zero :
∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
[inst_3 : FirstCountableTopology G], ∃ u, (nhds 0).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) + u (n + 1) ⊆ u n
This theorem states that for any topological additive group that is first countable, there exists an antitone neighborhood basis `u` for `nhds 0`, where `u` is a sequence of sets indexed by natural numbers such that for each `n`, the set `u (n + 1) + u (n + 1)` is contained in `u n`. The existence of such a basis is crucial for establishing that the quotient of an additive group by a topologically closed subgroup forms a complete space.
More concisely: For any first countable topological additive group, there exists an antitone sequence of neighborhoods of 0 with the property that the sum of any two consecutive sets is contained in each.
|
AddSubgroup.is_normal_topologicalClosure
theorem AddSubgroup.is_normal_topologicalClosure :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
(N : AddSubgroup G) [inst_3 : N.Normal], N.topologicalClosure.Normal
This theorem states that the topological closure of a normal additive subgroup is also a normal subgroup. In particular, for any type `G` that has a topology, supports addition, and is a topological additive group, and for any additive subgroup `N` of `G` that is normal, the topological closure of `N` will also be a normal subgroup.
More concisely: If `G` is a topological additive group and `N` is a normal additive subgroup of `G`, then the topological closure of `N` is also a normal subgroup of `G`.
|
eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup
theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
[inst_3 : TopologicalSpace α] [inst_4 : Zero α] [inst_5 : T1Space α] {f : G → α} {k : Set G},
IsCompact k → Function.support f ⊆ k → Continuous f → f = 0 ∨ LocallyCompactSpace G
This theorem states that if we have a function `f` from a topological additive group `G` to another topological space `α` with zero element, and the support of this function (the set of points where the function does not equal zero) is contained within a set `k` that is compact, then it implies that either the function `f` is trivial (i.e., it equals zero everywhere) or the group `G` is locally compact. The theorem also requires that the function `f` is continuous and that the space `α` satisfies the T1 separation axiom (every singleton set is closed).
More concisely: If a continuous function from a topological additive group to a T1 space with zero, whose support is a compact subset, is trivial if and only if the group is locally compact.
|
local_isCompact_isClosed_nhds_of_addGroup
theorem local_isCompact_isClosed_nhds_of_addGroup :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
[inst_3 : LocallyCompactSpace G] {U : Set G},
U ∈ nhds 0 → ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 0 ∈ interior K
The theorem `local_isCompact_isClosed_nhds_of_addGroup` states that in a locally compact topological additive group, for any neighborhood of the identity element, there exists a compact and closed neighborhood of the identity element that is contained within the original neighborhood, and the identity element belongs to the interior of this compact subset. This holds regardless of any separation properties of the topological space.
More concisely: In a locally compact topological additive group, for each neighborhood of the identity element, there exists a compact and closed subset containing the identity with the identity as an interior point.
|
compact_open_separated_mul_right
theorem compact_open_separated_mul_right :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : MulOneClass G] [inst_2 : ContinuousMul G] {K U : Set G},
IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 1, K * V ⊆ U
This theorem states that for a given type `G` equipped with a topology, a multiplication operation and a multiplicative identity, if `K` is a compact set and `U` is an open set such that `K` is a subset of `U`, then there exists an open neighborhood `V` of the multiplicative identity `1` such that the set resulting from the multiplication of every element of `K` with every element of `V` is still a subset of `U`. This result is significant in the study of topological groups and rings, where it is often important to understand how operations like multiplication interact with the topology.
More concisely: Given a topological group `(G, τ)` with a compact subset `K` and an open set `U` such that `K ⊆ U`, there exists an open neighborhood `V` of the identity `1` such that `K × V ⊆ U`.
|
Continuous.sub
theorem Continuous.sub :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G]
[inst_3 : TopologicalSpace α] {f g : α → G}, Continuous f → Continuous g → Continuous fun x => f x - g x
This theorem states that for any two functions `f` and `g` from a topological space `α` to another topological space `G`, if `f` and `g` are both continuous, then the function that subtracts the output of `g` from the output of `f` (for any input `x`) is also continuous. This is under the conditions that `G` has a subtraction operation and that subtraction is continuous. In mathematical terms, if `f` and `g` are continuous functions from `α` to `G`, and `G` is a topological algebra where subtraction is a continuous operation, then `(f - g)` is also a continuous function from `α` to `G`.
More concisely: If `f` and `g` are continuous functions from a topological space `α` to a topological algebra `G` where subtraction is continuous, then the function `x ↦ f(x) - g(x)` is continuous from `α` to `G`.
|
AddGroupTopology.continuous_add'
theorem AddGroupTopology.continuous_add' :
∀ {α : Type u} [inst : AddGroup α] (g : AddGroupTopology α), Continuous fun p => p.1 + p.2
This theorem, named `AddGroupTopology.continuous_add'`, states that for any type `α` that forms an additive group, given the topology `g` over this group, the addition operation is continuous. In other words, it asserts that in an additive group equipped with a certain topology, the map taking a pair of elements to their sum is continuous. This theorem version is designed to be used with dot notation.
More concisely: For any additive group (α, +) equipped with a topology g, the addition operation + is a continuous function.
|
continuous_of_continuousAt_zero
theorem continuous_of_continuousAt_zero :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G] {M : Type u_1}
{hom : Type u_2} [inst_3 : AddZeroClass M] [inst_4 : TopologicalSpace M] [inst_5 : ContinuousAdd M]
[inst_6 : FunLike hom G M] [inst_7 : AddMonoidHomClass hom G M] (f : hom), ContinuousAt (⇑f) 0 → Continuous ⇑f
This theorem states that for any additive monoid homomorphism `f`, which is a type of function mapping from an additive topological group `G` to an additive topological monoid `M`, if `f` is continuous at the point zero, then `f` is continuous everywhere. Here, continuity is defined in the topological sense, meaning that the limit of `f` as `x` approaches any point is equal to `f` at that point. The theorem uses the typeclass `FunLike` to ensure that the function `f` can be treated as a function from `G` to `M`, and the `AddMonoidHomClass` typeclass to ensure that `f` preserves the additive monoid structure. This theorem is a specific case of a more general fact about uniform continuity, as indicated by the reference to `uniformContinuous_of_continuousAt_zero`.
More concisely: If `f` is an additive monoid homomorphism from an additive topological group to an additive topological monoid, which is continuous at the identity element, then `f` is continuous everywhere.
|
AddSubgroup.properlyDiscontinuousVAdd_of_tendsto_cofinite
theorem AddSubgroup.properlyDiscontinuousVAdd_of_tendsto_cofinite :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
(S : AddSubgroup G),
Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G) → ProperlyDiscontinuousVAdd (↥S) G
This theorem states that for an additive topological group `G`, and a subgroup `S` of `G`, if the subgroup `S` is discrete (in the sense that the intersection of `S` with any compact set `K` is finite), then `S` acts on `G` through vector addition in a properly discontinuous manner. To be precise, if the function mapping each element of `S` to its corresponding element in `G` tends to have a cofinite filter (in which subsets have finite complements) mapped to a cocompact filter (generated by the complements of compact sets), then the left action of `S` on `G` is properly discontinuous. Here, a properly discontinuous action means that the stabilizer of each point is finite and the set of points moved by each element is locally finite.
More concisely: If a discrete subgroup of an additive topological group acts on the group through vector addition and tends to have a cofinite filter mapped to a cocompact filter, then the action is properly discontinuous.
|
Filter.Tendsto.div'
theorem Filter.Tendsto.div' :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Div G] [inst_2 : ContinuousDiv G] {f g : α → G}
{l : Filter α} {a b : G},
Filter.Tendsto f l (nhds a) →
Filter.Tendsto g l (nhds b) → Filter.Tendsto (fun x => f x / g x) l (nhds (a / b))
The theorem `Filter.Tendsto.div'` states that if `f` and `g` are functions from a type `α` to a topological space `G` equipped with a division operation and continuous division, and `l` is a filter on `α`, then if `f` tends towards a point `a` and `g` tends towards a point `b` (i.e., for every neighborhood of `a` and `b`, the preimage under `f` and `g` respectively is a neighborhood of `l`), then the function that sends `x` to `f(x) / g(x)` tends towards the point `a / b`. In other words, the limits of the ratios of the function values at a point is the ratio of the limits of the functions, provided all the limits exist and the limit of the denominator function is not zero.
More concisely: If functions `f` and `g` from type `α` to topological space `G` with continuous division are such that `f` tends to `a` and `g` tends to a nonzero `b`, then their ratio function `x ↦ f(x) / g(x)` tends to `a / b`.
|
ContinuousOn.sub
theorem ContinuousOn.sub :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G]
[inst_3 : TopologicalSpace α] {f g : α → G} {s : Set α},
ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => f x - g x) s
The `ContinuousOn.sub` theorem states that for any topological space `G` and any type `α`, given `G` has a subtraction operation and is continuous under subtraction, and given another topological space `α`, if the functions `f` and `g` from `α` to `G` are continuous on a set `s`, then the function which maps `x` in `α` to the difference `f(x) - g(x)` in `G` is also continuous on this set `s`. This theorem is a formalization of the property of continuous functions in topology that the difference of two continuous functions is again a continuous function.
More concisely: If `G` is a topological space with continuous subtraction and `f` and `g` are continuous functions from a set `s` in another topological space `α` to `G`, then the function `x ↦ f(x) - g(x)` is continuous on `s`.
|
IsClosed.vadd_left_of_isCompact
theorem IsClosed.vadd_left_of_isCompact :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup α]
[inst_3 : AddAction α β] [inst_4 : ContinuousNeg α] [inst_5 : ContinuousVAdd α β] {s : Set α} {t : Set β},
IsClosed t → IsCompact s → IsClosed (s +ᵥ t)
The theorem `IsClosed.vadd_left_of_isCompact` states that for any two types `α` and `β` with `α` being an additive group and `β` an additive action of `α`, given topological spaces over `α` and `β`, and provided that the negation in `α` and vector addition in `β` are continuous functions, if `s` is a compact set in `α` and `t` is a closed set in `β`, then the vector addition of `s` and `t` (denoted as `s +ᵥ t`) is also a closed set in `β`. This theorem links the concepts of compactness and closedness under the operation of vector addition.
More concisely: If `α` is an additive group, `β` is an additive action of `α`, and negation and vector addition in `β` are continuous, then the Minkowski sum of a compact set in `α` and a closed set in `β` is a closed set in `β`.
|
TopologicalGroup.exists_antitone_basis_nhds_one
theorem TopologicalGroup.exists_antitone_basis_nhds_one :
∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : FirstCountableTopology G], ∃ u, (nhds 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
The theorem `TopologicalGroup.exists_antitone_basis_nhds_one` asserts that in any first countable topological group, there exists an antitone (decreasing or non-increasing) neighborhood basis `u` for the neighborhood of the identity element such that the square of `u(n + 1)` is a subset of `u(n)`. This means that, given any natural number `n`, the set formed by taking all possible products of two elements from `u(n + 1)` is included in the set `u(n)`. The existence of such a neighborhood basis is a crucial tool for establishing the completeness of quotient groups in the context of topological groups.
More concisely: In any first countable topological group, there exists an antitone neighborhood basis for the identity element such that the square of each successive basis forms a subset of the previous one.
|
instLocallyCompactSpaceOfWeaklyOfGroup
theorem instLocallyCompactSpaceOfWeaklyOfGroup :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : WeaklyLocallyCompactSpace G], LocallyCompactSpace G
This theorem states that for any type `G` that has a topological space structure, a group structure, a topological group structure, and is weakly locally compact, `G` will also have a locally compact space structure. In other words, if we have a topological group that is weakly locally compact, it is guaranteed to be locally compact.
More concisely: If a topological group `G` has a weakly locally compact topology, then `G` has a locally compact topology.
|
Filter.Tendsto.neg
theorem Filter.Tendsto.neg :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : ContinuousNeg G] {f : α → G}
{l : Filter α} {y : G}, Filter.Tendsto f l (nhds y) → Filter.Tendsto (fun x => -f x) l (nhds (-y))
The theorem `Filter.Tendsto.neg` states that for any given function `f` mapping from a type `α` to a type `G`, if `f` converges to a value `y` in a topological space `G` that also forms an additive group with a continuous negation operation, then the function that maps each value `x` in the domain to the negation of `f(x)` converges to the negation of `y`. In other words, if a function's values approach some `y` as the input is filtered through a particular filter `l`, then the values of the negated function also approach the negation of `y` under the same input filter.
More concisely: If a function from a topological space to an additive group with a continuous negation converges to a value under a filter, then the negated function converges to the negation of that value under the same filter.
|
AddGroupTopology.continuous_neg'
theorem AddGroupTopology.continuous_neg' :
∀ {α : Type u} [inst : AddGroup α] (g : AddGroupTopology α), Continuous Neg.neg
The theorem `AddGroupTopology.continuous_neg'` states that for any given type `α` that forms an addition group (denoted by `AddGroup α`), and for any topology `g` on that addition group (denoted by `AddGroupTopology α`), the negation function (denoted by `Neg.neg`) is continuous. In mathematical terms, this means that the opposite operation is a continuous function in the topology defined on the group. This is a version of the global `continuous_neg` that can be used with dot notation.
More concisely: For any addition group `α` with topology `g`, the negation function `Neg.neg` is a continuous map from `(AddGroupTopology α, τ)` to itself, where `τ` is the discrete topology on `α`.
|
compact_open_separated_add_left
theorem compact_open_separated_add_left :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddZeroClass G] [inst_2 : ContinuousAdd G] {K U : Set G},
IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 0, V + K ⊆ U
The theorem `compact_open_separated_add_left` states that for any type `G` with a topological space structure, addition with zero, and continuous addition, given a compact set `K` and an open set `U` in `G` such that `K` is a subset of `U`, there exists an open neighborhood `V` of `0` (in the topological sense) such that the sum of `V` and `K` is a subset of `U`. In plain terms, for a compact set inside an open set, we can find an open neighborhood around zero such that when we add this neighborhood to the compact set, we stay within the original open set.
More concisely: For any compact subset $K$ of a topological space $(G, \tau)$ with addition and a continuous addition function, there exists an open neighborhood $V$ of $0$ such that $K + V \subseteq U$, given $U$ is an open set containing $K$.
|
ContinuousAt.neg
theorem ContinuousAt.neg :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : ContinuousNeg G]
[inst_3 : TopologicalSpace α] {f : α → G} {x : α}, ContinuousAt f x → ContinuousAt (fun x => -f x) x
The theorem `ContinuousAt.neg` states that for any topological spaces `G` and `α`, a function `f` from `α` to `G`, and a point `x` in `α`, if the function `f` is continuous at the point `x`, then the function that sends `x` to the negation of `f(x)` is also continuous at `x`. Here, `Neg G` denotes that the type `G` has a negation operation, and `ContinuousNeg G` asserts that this negation operation is continuous.
More concisely: If `f : α → G` is continuous at `x ∈ α` in a topological space `(α,τα)` with negation `Neg G`, then the function `x mapsto -f(x)` is continuous at `x`.
|
compact_covered_by_add_left_translates
theorem compact_covered_by_add_left_translates :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G] {K V : Set G},
IsCompact K → (interior V).Nonempty → ∃ t, K ⊆ ⋃ g ∈ t, (fun x => g + x) ⁻¹' V
The theorem `compact_covered_by_add_left_translates` states that for any type `G` that is a topological space, an additive group, and a topological additive group, and any sets `K` and `V` of this type, if `K` is a compact set and `V` has a non-empty interior, then there exists a set `t` such that `K` is contained within the union of the inverse image of `V` under the function that adds an element of `t` to `x`, for each element `g` in `t`. In other words, a compact set can be covered by finitely many left additive translates of a set with non-empty interior.
More concisely: A compact subset of a topological additive group can be covered by finitely many left translates of a subset with non-empty interior.
|
ContinuousAt.sub
theorem ContinuousAt.sub :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G]
[inst_3 : TopologicalSpace α] {f g : α → G} {x : α},
ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun x => f x - g x) x
The theorem `ContinuousAt.sub` states that for any two functions `f` and `g` from a type `α` to a type `G`, where `G` is a topological space with a subtraction operation and a continuous subtraction operation, and `α` is also a topological space, if both `f` and `g` are continuous at a point `x` in `α`, then the function that sends `x` to the difference `f(x) - g(x)` is also continuous at `x`. This is essentially stating that the operation of subtraction preserves continuity.
More concisely: If `f` and `g` are continuous functions from a topological space `α` to a topological space `G` with a continuous subtraction operation, then their pointwise difference `x ↦ f(x) - g(x)` is also continuous at every point `x` in `α`.
|
IsCompact.locallyCompactSpace_of_mem_nhds_of_group
theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] {K : Set G},
IsCompact K → ∀ {x : G}, K ∈ nhds x → LocallyCompactSpace G
This theorem states that in the context of a topological group, if a point has a compact neighborhood, then the group is locally compact. More specifically, for any type `G` which has a topological space structure, a group structure, and a topological group structure, if a subset `K` of `G` is compact and `K` is a neighborhood of some point `x` in `G`, then `G` is a locally compact space. In mathematical terms, this means that for every point in the group, there exists a compact neighborhood, which is a fundamental notion in topology and analysis.
More concisely: In a topological group, if every point has a compact neighborhood, then the group is locally compact.
|
subset_add_closure_zero
theorem subset_add_closure_zero :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] (s : Set G), s ⊆ s + closure {0}
This theorem states that for any type `G` which is a topological space and an additive group, and for any set `s` of type `G`, `s` is a subset of the set obtained by adding `s` and the closure of the singleton set containing only the additive identity (0). In simpler terms, every element of `s` is also an element of the set formed by adding `s` and the closure of the set containing just 0.
More concisely: For any topological additive group `G` and subset `s` of `G`, `s` is contained in the set `s ∪ {0} ⊔ cl {0}`, where `cl` denotes the topological closure and `⊔` denotes the set union with the closure.
|
exists_isCompact_isClosed_subset_isCompact_nhds_one
theorem exists_isCompact_isClosed_subset_isCompact_nhds_one :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] {L : Set G},
IsCompact L → L ∈ nhds 1 → ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ L ∧ K ∈ nhds 1
This theorem states that in any topological group, if there exists a compact neighborhood of the identity element (denoted as `1`), then there also exists a subset of this neighborhood which is both compact and closed, and is also a neighborhood of the identity. The topological group is given by the type `G` with the associated topological space and group structures, and the neighborhood is represented by a set `L`. If `L` is compact and is a neighborhood of the identity, the theorem asserts the existence of a subset `K` which satisfies the stated properties.
More concisely: In any topological group, if there exists a compact neighborhood of the identity, then there exists a compact and closed subset of that neighborhood that is also a neighborhood of the identity.
|
Continuous.neg
theorem Continuous.neg :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : ContinuousNeg G]
[inst_3 : TopologicalSpace α] {f : α → G}, Continuous f → Continuous fun x => -f x
This theorem states that for any topological space `G` and any other type `α` with a continuous function `f : α → G`, if `G` supports negation operation and this negation operation is continuous, then the function that applies negation to the result of `f`, i.e., `-f x`, is also continuous. In mathematical parlance, if `f` is continuous and `G` is a topological space with a continuous negation, then the composition of `f` with the negation function is also continuous.
More concisely: If `f : α → G` is a continuous function from a type `α` to a topological space `G` with a continuous negation operation, then the function `-f : α → G` defined by `-f x := -(f x)` is continuous.
|
Continuous.div'
theorem Continuous.div' :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Div G] [inst_2 : ContinuousDiv G]
[inst_3 : TopologicalSpace α] {f g : α → G}, Continuous f → Continuous g → Continuous fun x => f x / g x
This theorem states that for any two continuous functions `f` and `g` that map from a certain type `α` to a type `G`, the function that maps `x` to the quotient of `f(x)` and `g(x)` is also continuous. This is the case for all `G` that are topological spaces and have defined division operation, and for all `α` that are topological spaces. The continuity of division in `G` (`ContinuousDiv G`) is also required.
More concisely: If `f` and `g` are continuous functions from a topological space `α` to the topological space `G` with a defined division operation and continuous division, then the function that maps `x` to the quotient `f(x) / g(x)` is continuous.
|
TopologicalAddGroup.continuous_conj
theorem TopologicalAddGroup.continuous_conj :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : Add G] [inst_3 : ContinuousAdd G] (g : G),
Continuous fun h => g + h + -g
This theorem states that for any type `G` (with an associated `TopologicalSpace`, `Neg` (negation), and `Add` (addition) structure, and where addition is a continuous operation), conjugation by a fixed element `g` is a continuous function. In other words, for any fixed `g` in `G`, the function that takes `h` to `g + h - g` (i.e., adding `g` to `h` and then subtracting `g`) is a continuous function. This holds when we are working in a topological group where addition is a continuous operation.
More concisely: Given a topological group `G` with a continuous addition operation, the function `x => g + x - g` is a continuous conjugation by `g` for any fixed `g` in `G`.
|
ContinuousOn.neg
theorem ContinuousOn.neg :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : ContinuousNeg G]
[inst_3 : TopologicalSpace α] {f : α → G} {s : Set α}, ContinuousOn f s → ContinuousOn (fun x => -f x) s
The theorem `ContinuousOn.neg` states that for any topological space `G` and any type `α`, given a function `f` from `α` to `G` that is continuous on a set `s` of `α`, and provided `G` has a negation operation that is continuous, then the function that sends `x` to the negation of `f(x)` is also continuous on `s`. In other words, negating a continuous function on a topological space yields another continuous function on that space, assuming the negation operation itself is continuous.
More concisely: If a continuous function from a set to a topological space with a continuous negation operation is defined on a subset, then the function sending each element to the negation of its image under the original function is also continuous on that subset.
|
continuous_sub_left
theorem continuous_sub_left :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G] (a : G),
Continuous fun x => a - x
This theorem states that for any type `G` that has a topological structure (i.e., `G` is a topological space), a subtraction operation (`Sub G`), and the subtraction operation is continuous (`ContinuousSub G`), then for any given element `a` of type `G`, the function that subtracts each element `x` in `G` from `a` is a continuous function. This essentially says that subtraction from a fixed element in a topological group with continuous subtraction is a continuous operation.
More concisely: If `G` is a topological space with a continuous subtraction operation, then for any `a` in `G`, the function `x ↦ a - x` is a continuous function from `G` to `G`.
|
TopologicalAddGroup.continuous_conj'
theorem TopologicalAddGroup.continuous_conj' :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : Add G] [inst_3 : ContinuousAdd G]
[inst_4 : ContinuousNeg G] (h : G), Continuous fun g => g + h + -g
This theorem states that in the context of a topological space `G` equipped with negation (`Neg`), addition (`Add`), and where both addition and negation are continuous functions (`ContinuousAdd` and `ContinuousNeg`), for any fixed element `h` of `G`, the function `fun g => g + h + -g` (which represents the process of conjugation) is continuous. In other words, it's saying that the action of conjugation on a fixed element of the additive group is a continuous operation provided that both addition and negation in the group are continuous.
More concisely: In a topological additive group equipped with continuous negation and addition, the function mapping each element to its conjugate with respect to a fixed element is a continuous function.
|
Filter.Tendsto.sub
theorem Filter.Tendsto.sub :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G] {f g : α → G}
{l : Filter α} {a b : G},
Filter.Tendsto f l (nhds a) →
Filter.Tendsto g l (nhds b) → Filter.Tendsto (fun x => f x - g x) l (nhds (a - b))
This theorem, `Filter.Tendsto.sub`, states that for any types `G` and `α`, where `G` is a topological space with subtraction operation and this subtraction operation is continuous, if we have two functions `f` and `g` from `α` to `G`, a filter `l` on `α`, and two elements `a` and `b` in `G`, such that `f` tends to `a` and `g` tends to `b` with respect to the filter `l` (i.e., for any neighborhood of `a` or `b`, the preimage under `f` or `g` respectively is a neighborhood in the filter `l`), then the function that takes `x` to `f(x) - g(x)` tends to `a - b` with respect to the filter `l`. In simpler terms, if `f` and `g` both converge to `a` and `b` respectively under the filter `l`, then the difference of `f` and `g` also converges to the difference of `a` and `b` under the same filter. This is an encapsulation of the basic property of limits where the limit of the difference of two functions is the difference of the limits, provided both limits exist.
More concisely: Given topological spaces G with continuous subtraction, functions f and g from type α to G, and filter l on α such that f tends to a and g tends to b with respect to l, then f - g tends to a - b with respect to l.
|
Subgroup.is_normal_topologicalClosure
theorem Subgroup.is_normal_topologicalClosure :
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] (N : Subgroup G)
[inst_3 : N.Normal], N.topologicalClosure.Normal
This theorem states that the topological closure of a normal subgroup is also a normal subgroup. In the context of the theorem, `G` is a topological group, which is a group equipped with a topology that is compatible with the group operation. `N` is a normal subgroup of `G`. The theorem asserts that if `N` is a normal subgroup of `G`, then the topological closure of `N` (denoted as `N.topologicalClosure`) is also a normal subgroup.
More concisely: In a topological group, the topological closure of a normal subgroup is a normal subgroup.
|
IsOpen.add_closure
theorem IsOpen.add_closure :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G] {s : Set G},
IsOpen s → ∀ (t : Set G), s + closure t = s + t
The theorem `IsOpen.add_closure` states that for any type `G` which has a topological space structure, an additive group structure and a topological additive group structure, and for any open set `s` in `G`, the sum of `s` and the closure of any set `t` in `G` is equal to the sum of `s` and `t`. This property is important in the study of topological groups, where the algebraic operations interact with the topology in a continuous way.
More concisely: For any topological additive group `(G, ⊓, +)`, and open set `s` in `G`, the sum of `s` and the closure of any set `t` in `G` is equal to the sum of `s` and `t`.
|
exists_closed_nhds_zero_neg_eq_add_subset
theorem exists_closed_nhds_zero_neg_eq_add_subset :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G] {U : Set G},
U ∈ nhds 0 → ∃ V ∈ nhds 0, IsClosed V ∧ -V = V ∧ V + V ⊆ U
This theorem states that for any topological add group `G`, given a neighborhood `U` of the identity element `0`, there exists another neighborhood `V` of the identity `0` with three properties: `V` is closed, `V` is symmetric (i.e., `-V = V`), and the sum of `V` with itself is a subset of `U` (i.e., `V + V ⊆ U`).
More concisely: For any topological add group `G` and neighborhood `U` of its identity `0`, there exists a symmetric, closed neighborhood `V` of `0` such that `V + V ⊆ U`.
|
GroupTopology.continuous_inv'
theorem GroupTopology.continuous_inv' : ∀ {α : Type u} [inst : Group α] (g : GroupTopology α), Continuous Inv.inv := by
sorry
The theorem `GroupTopology.continuous_inv'` asserts that for any given type `α` that has a group structure, signified by `[inst : Group α]`, and for any given group topology `g` on this type, the function that assigns to each element of the group its inverse, denoted by `Inv.inv`, is a continuous function. This is a version of the more general `continuous_inv` theorem that is amenable to the use of dot notation.
More concisely: For any group `α` with group topology `g`, the function that maps each element `x` to its inverse is a continuous function. (written as `continuous (Inv.inv) : Continuous (Inv.inv) α`)
|
inv_closure
theorem inv_closure :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [inst_2 : ContinuousInv G] (s : Set G),
(closure s)⁻¹ = closure s⁻¹
The theorem `inv_closure` states that for any set `s` of elements of type `G`, where `G` is a type equipped with a topology, an involutive inverse operation, and where this inverse operation is continuous, the closure of the inverse of `s` (i.e., `(closure s)⁻¹`) is equal to the inverse of the closure of `s` (i.e., `closure s⁻¹`). This means that taking the closure and taking the inverse of a set can be interchanged without affecting the result.
More concisely: For any topological space `(G, top)` with an involutive, continuous inverse operation, the closure of the inverse of a set `s` equals the inverse of the closure of `s`: `(closure s)⁻¹ = closure s⁻¹`.
|
AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite
theorem AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
(S : AddSubgroup G),
Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G) → ProperlyDiscontinuousVAdd (↥S.op) G
This theorem states that for any additive subgroup `S` of a topological additive group `G`, if the function mapping elements in `S` to `G` (denoted by `⇑S.subtype`) tends to the filter generated by complements to compact sets (`Filter.cocompact G`) when applied to the filter of subsets whose complements are finite (`Filter.cofinite`), then `S` acts on `G` properly discontinuously on the right. Here, `S` acting properly discontinuously on the right means that `S` is discrete in the sense that the intersection of `S` and any compact set `K` is finite. If `G` is a Hausdorff space, this theorem can be combined with `t2Space_of_properlyDiscontinuousVAdd_of_t2Space` to show that the quotient group `G/S` is also a Hausdorff space.
More concisely: If an additive subgroup `S` of a topological additive group `G` such that the image of `S` under the subtype function tends to the filter of cocompact sets when applied to the filter of cofinite sets, then `S` acts properly discontinuously on the right in `G`.
|
exists_disjoint_vadd_of_isCompact
theorem exists_disjoint_vadd_of_isCompact :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
[inst_3 : NoncompactSpace G] {K L : Set G}, IsCompact K → IsCompact L → ∃ g, Disjoint K (g +ᵥ L)
The given theorem asserts that in a noncompact additive topological group, for any two compact sets, there exists a translation of the second set that is disjoint from the first set. In other words, it is possible to shift the second set by some group element such that the shifted set and the first set do not share any common elements. This result applies to the setting where the underlying topological space is a group with a continuous group operation (an additive topological group) that is not compact (a NoncompactSpace).
More concisely: In a noncompact additive topological group, for any two compact sets, there exists a translation that makes them disjoint.
|
TopologicalGroup.continuous_conj_prod
theorem TopologicalGroup.continuous_conj_prod :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : Mul G] [inst_3 : ContinuousMul G]
[inst_4 : ContinuousInv G], Continuous fun g => g.1 * g.2 * g.1⁻¹
This theorem states that for any type `G` that has a topological space structure, an inversion operation, a multiplication operation, and both multiplication and inversion are continuous functions, the function representing the conjugation operation, `(g.1 * g.2 * g.1⁻¹)`, is also continuous. Conjugation here takes two elements from `G`, multiplies the first by the second, and then multiplies the result by the inverse of the first element.
More concisely: For any topological group `G` with continuous multiplication and inversion operations, the conjugation function `(g.1 * g.2 * g.1⁻¹)` is a continuous function.
|
neg_closure
theorem neg_closure :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : ContinuousNeg G] (s : Set G),
-closure s = closure (-s)
This theorem, `neg_closure`, states that for any type `G` that has a topology, an involutive negation operation, and where this negation operation is continuous, the closure of the negation of a set `s` is equal to the negation of the closure of `s`. This is to say, if `s` is a set in `G`, then the closure operation and the negation operation commute. It means that applying the closure on the negation of the set is the same as first applying the closure on the set and then applying the negation. The theorem holds true for all such types `G` and all sets `s` of type `G`.
More concisely: For any topological space `(G, τ)` with an involutive continuous negation operation, the closure of the negation of a set `s ⊆ G` equals the negation of the closure of `s`, i.e., `cl(¬s) = ¬(cl(s))`.
|
Continuous.inv
theorem Continuous.inv :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : ContinuousInv G]
[inst_3 : TopologicalSpace α] {f : α → G}, Continuous f → Continuous fun x => (f x)⁻¹
This theorem states that for any two types `G` and `α`, where `G` is a topological space that supports inversion operation (`Inv`) and it's continuous (`ContinuousInv`), and `α` is another topological space, if a function `f` from `α` to `G` is continuous (`Continuous f`), then the function that applies the inversion to each output of `f` is also continuous. In mathematical terms, if `f` is a continuous function mapping from a topological space `α` to a topological space `G` that supports a continuous inversion operation, then the function `g` defined by `g(x) = (f(x))⁻¹` for all `x` in `α` is also continuous.
More concisely: If `f` is a continuous function from a topological space `α` to a topological space `G` with a continuous inversion operation, then the function `g(x) = (f(x))⁻¹` is also continuous.
|
TopologicalGroup.continuous_conj'
theorem TopologicalGroup.continuous_conj' :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : Mul G] [inst_3 : ContinuousMul G]
[inst_4 : ContinuousInv G] (h : G), Continuous fun g => g * h * g⁻¹
This theorem states that in a topological group `G`, the operation of conjugation on a fixed element `h` of the group is a continuous function. Here a topological group is a group `G` that is also a topological space such that the group's multiplication and inversion operations are continuous. In terms of the group operation, the conjugation of `h` by an element `g` is defined as `g * h * g⁻¹`, and this theorem asserts that if `h` is a fixed element of `G`, then the function `g ↦ g * h * g⁻¹` is continuous.
More concisely: In a topological group, the conjugation map `g ↦ g * h * g⁻¹` is a continuous function for any fixed element `h`.
|
local_isCompact_isClosed_nhds_of_group
theorem local_isCompact_isClosed_nhds_of_group :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G]
[inst_3 : LocallyCompactSpace G] {U : Set G},
U ∈ nhds 1 → ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 1 ∈ interior K
This theorem states that in a locally compact group, for any neighborhood of the identity element, there exists a compact and closed neighborhood of the identity that is contained within the given neighborhood. Moreover, the identity element itself belongs to the interior of this compact, closed neighborhood. This property holds even without requiring any separation assumptions on the space.
In other words, given any neighborhood of the identity in a locally compact group , we can always find a compact and closed subset of it, which still contains the identity in its interior. This theorem is fundamental in the study of locally compact groups and their topological properties.
More concisely: In a locally compact group, for any neighborhood of the identity, there exists a compact and closed subset containing the identity with the identity in its interior.
|
nhds_translation_mul_inv
theorem nhds_translation_mul_inv :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] (x : G),
Filter.comap (fun x_1 => x_1 * x⁻¹) (nhds 1) = nhds x
This theorem is about topological groups, which are groups that also have a topological structure compatible with the group operations. The theorem states that for every element `x` of a topological group `G`, the preimage under the function `(fun x_1 => x_1 * x⁻¹)` of the neighborhood filter of the group's identity element `1` is equal to the neighborhood filter of `x` itself. In other words, multiplying each element of the neighborhood of the identity by `x` and taking the inverse gives us the neighborhood of `x`.
More concisely: For every topological group G and element x in G, the preimage under the function x ↦ x\_1 \* x^(-1) of the neighborhood filter of G's identity element 1 is equal to the neighborhood filter of x.
|
compact_open_separated_add_right
theorem compact_open_separated_add_right :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddZeroClass G] [inst_2 : ContinuousAdd G] {K U : Set G},
IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 0, K + V ⊆ U
This theorem states that for any given compact set `K` that is a subset of an open set `U` in a topological space `G` that has a zero element and addition operation that is continuous, there exists an open neighborhood `V` of `0` such that the sum of the set `K` and `V` is a subset of `U`. In other words, if `K` is compact and contained in an open set `U`, we can find an open neighborhood around zero, such that when we add this neighborhood to every element in `K`, all the resulting elements still remain within `U`.
More concisely: Given a compact subset `K` of an open set `U` in a topological space with a continuous addition operation and zero element, there exists an open neighborhood `V` of the zero element such that `K + V ⊆ U`.
|
HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup
theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
[inst_3 : TopologicalSpace α] [inst_4 : Zero α] [inst_5 : T1Space α] {f : G → α},
HasCompactSupport f → Continuous f → f = 0 ∨ LocallyCompactSpace G
The theorem `HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup` states that, for any function `f` from a topological additive group `G` to a `T1` topological space `α` that takes `0` as a value, if `f` has compact support and is continuous, then one of two conditions must be true: either `f` is the zero function (i.e., it maps every element of `G` to `0`), or the topological additive group `G` is locally compact.
More concisely: A continuous function from a topological additive group with compact support to a T1 space mapping 0 to itself is either the zero function or defines a locally compact group.
|
map_add_left_nhds_zero
theorem map_add_left_nhds_zero :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G] (x : G),
Filter.map (fun x_1 => x + x_1) (nhds 0) = nhds x
The theorem `map_add_left_nhds_zero` states that for any type `G` that has a topological space structure, an additive group structure, and a topological additive group structure, we have for any element `x` of `G`, the filter obtained by mapping `(fun x_1 => x + x_1)` to the neighborhood filter of `0` is equal to the neighborhood filter of `x`. In other words, applying the mapping function that adds `x` to every element to the neighborhood filter of zero gives the neighborhood filter of `x`. This is an important property in topological additive groups.
More concisely: For any topological additive group (G, +, 0), the mapping (x ↦ x + 0) preserves neighborhood filters, i.e., the neighborhood filter of 0 in G maps to the neighborhood filter of x.
|
Filter.Tendsto.sub_const
theorem Filter.Tendsto.sub_const :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G] {c : G}
{f : α → G} {l : Filter α},
Filter.Tendsto f l (nhds c) → ∀ (b : G), Filter.Tendsto (fun x => f x - b) l (nhds (c - b))
In natural language, the theorem `Filter.Tendsto.sub_const` states that for any given type `G` which has a topological structure, a subtraction operation, and satisfies the property of continuous subtraction, and for a given constant `c` of type `G`, a function `f` from type `α` to `G`, and a filter `l` on `α`. If `f` tends to the neighborhood filter of `c` as `l` tends to infinity (expressed as `Filter.Tendsto f l (nhds c)`), then for any constant `b` of type `G`, the function `f x - b` also tends to the neighborhood filter of `c - b` as `l` tends to infinity (expressed as `Filter.Tendsto (fun x => f x - b) l (nhds (c - b))`). This theorem is essentially stating a property of limits in a topological space where the limit of a function minus a constant is equal to the limit of the function minus the same constant.
More concisely: If `f` tends to `c` as `l` approaches infinity, then `f(x) - c` tends to `0` as `l` approaches infinity for all `x`, i.e., `Filter.Tendsto f l (nhds c)` implies `Filter.Tendsto (fun x => f x - c) l (nhds 0)` in a topological space with continuous subtraction.
|
compact_covered_by_mul_left_translates
theorem compact_covered_by_mul_left_translates :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] {K V : Set G},
IsCompact K → (interior V).Nonempty → ∃ t, K ⊆ ⋃ g ∈ t, (fun x => g * x) ⁻¹' V
The theorem `compact_covered_by_mul_left_translates` states that for any topological group `G`, if `K` is a compact set and `V` is a set with non-empty interior, then there exists a set `t` such that `K` is covered by the union of the left multiplicative translates of `V` over all elements of `t`. In simpler terms, we can shift `V` by multiplying its elements by each element of `t` on the left, and the union of these shifted sets will contain all elements of `K`. Here, a topological group is a group that is also a topological space, such that the group's operations are continuous functions, and a left multiplicative translate of a set by a group element is the set obtained by multiplying each element of the set by the group element on the left.
More concisely: Given a topological group G, if K is a compact subset and V has non-empty interior, then there exists a set t in G such that K is covered by the union of the left translates of V by elements in t.
|
exists_isCompact_isClosed_subset_isCompact_nhds_zero
theorem exists_isCompact_isClosed_subset_isCompact_nhds_zero :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G] {L : Set G},
IsCompact L → L ∈ nhds 0 → ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ L ∧ K ∈ nhds 0
The theorem `exists_isCompact_isClosed_subset_isCompact_nhds_zero` states that for any type `G` that has a topological space structure, an additive group structure, and a topological additive group structure, given a set `L` of `G` that is compact and a neighborhood of `0`, there exists a closed, compact subset `K` of `L` that is also a neighborhood of `0`. In other words, any compact neighborhood of `0` in a topological additive group contains a closed compact subset that is a neighborhood of `0`.
Note that a set `L` is a neighborhood of `0` in this context if it contains an open set around `0`. A set is compact if for any nontrivial filter that contains the set, there exists an element such that every set of the filter intersects every neighborhood of that element. A set is closed if it contains all its limit points.
More concisely: In a topological additive group, any compact neighborhood of 0 contains a closed and compact subset that is also a neighborhood of 0.
|
continuous_of_continuousAt_one
theorem continuous_of_continuousAt_one :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] {M : Type u_1}
{hom : Type u_2} [inst_3 : MulOneClass M] [inst_4 : TopologicalSpace M] [inst_5 : ContinuousMul M]
[inst_6 : FunLike hom G M] [inst_7 : MonoidHomClass hom G M] (f : hom), ContinuousAt (⇑f) 1 → Continuous ⇑f
The theorem `continuous_of_continuousAt_one` asserts that in the context of topological groups and monoids, if we have a monoid homomorphism (which is a function preserving monoid structure) from a topological group to a topological monoid, and this homomorphism is continuous at the identity element of the group, then this homomorphism is continuous everywhere. In simpler terms, if the transformation of group elements to monoid elements doesn't cause "jumps" when you infinitesimally nudge the group element around the identity, then there won't be any "jumps" anywhere else either.
More concisely: If a monoid homomorphism from a topological group to a topological monoid is continuous at the group identity, then it is continuous everywhere.
|
continuous_zsmul
theorem continuous_zsmul :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G] (z : ℤ),
Continuous fun a => z • a
This theorem states that for any integer `z`, the operation of multiplying an element `a` from a topological additive group `G` by `z` (denoted as `z • a`) is a continuous function. Here, `G` is a type equipped with a topology (making it a topological space) and an additive group structure, and it's also assumed that the group operation is continuous with respect to the topology (making `G` a topological additive group).
More concisely: For any topological additive group (G, +) with continuous group operation and any integer z, the function multiplication by z: G -> G, a => z * a, is a continuous function.
|
Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite
theorem Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] (S : Subgroup G),
Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G) → ProperlyDiscontinuousSMul (↥S) G
This theorem states that for any subgroup `S` of a topological group `G`, if the function that maps each element of `S` to its corresponding element in `G` tends to take cofinite subsets (sets whose complements are finite) to cocompact subsets (complements of compact sets) in `G`, then `S` acts on `G` properly discontinuously on the left. This action is properly discontinuous if `S` is discrete, which means `S` intersects with every compact subset of `G` in a finite set. This condition is related to the concept of `DiscreteTopology`.
More concisely: If a subgroup of a topological group maps cofinite subsets to cocompact subsets, then it acts properly discontinuously on the left.
|
Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite
theorem Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] (S : Subgroup G),
Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G) → ProperlyDiscontinuousSMul (↥S.op) G
The theorem `Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite` states that for any given topological group `G` with a subgroup `S`, if the function mapping elements of `S` to `G` tends to the filter generated by complements to compact sets (in this context, `Filter.cocompact G`) when the input values approach those sets whose complements are finite (`Filter.cofinite`), then `S` acts on `G` properly discontinuously on the right. Here, a properly discontinuous action means that `S` is discrete in the sense that the intersection of `S` and any compact set `K` in `G` is finite. This theorem is particularly useful when `G` is a Hausdorff space, as it can be combined with other results to show that the quotient group `G/S` inherits the Hausdorff property.
More concisely: If a subgroup `S` of a topological group `G` makes the function from `S` to `G` tend to the filter of complements of cocompact sets as inputs approach sets with finite complements, then `S` acts properly discontinuously on the right in `G`.
|
TopologicalAddGroup.ext
theorem TopologicalAddGroup.ext :
∀ {G : Type u_1} [inst : AddGroup G] {t t' : TopologicalSpace G},
TopologicalAddGroup G → TopologicalAddGroup G → nhds 0 = nhds 0 → t = t'
This theorem states that for any type `G` equipped with an additive group structure, and two topological structures `t` and `t'` on `G`, if `G` is a topological additive group under both `t` and `t'` and the neighborhood filters at zero for both `t` and `t'` coincide, then these two topological structures `t` and `t'` must be the same. In other words, the topological structure on a topological additive group is uniquely determined by the neighborhood filter at zero.
More concisely: Given a topological additive group `G` with two topologies `t` and `t'` having identical zero-neighborhood filters, `t` equals `t'`.
|
GroupTopology.continuous_mul'
theorem GroupTopology.continuous_mul' :
∀ {α : Type u} [inst : Group α] (g : GroupTopology α), Continuous fun p => p.1 * p.2
This theorem, named `GroupTopology.continuous_mul'`, states that for any type `α` that forms a Group, and for any instance `g` of `GroupTopology` on `α`, the multiplication operation, which takes a pair of elements and returns their product, is continuous. Here, continuity is a topological property that means intuitively that small changes in the input result in small changes in the output. This particular version of `continuous_mul` is formatted for use with dot notation in Lean.
More concisely: For any group (α, +) with a group topology instance g, the group multiplication operation is continuous.
|
continuous_zpow
theorem continuous_zpow :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G] (z : ℤ),
Continuous fun a => a ^ z
This theorem states that for any integer `z`, the function that raises a given element `a` of a topological group `G` to the power `z` is a continuous function. Here, `G` is not just any type, but a type equipped with a topology (i.e., a topological space) and a group structure (i.e., it's a group), and these two structures are compatible in a sense that `G` is a topological group. In other words, the theorem says that integer power is a continuous operation in a topological group.
More concisely: For any topological group (G, ±) and integer z, the function x ↦ x^z is a continuous homomorphism.
|
QuotientAddGroup.nhds_eq
theorem QuotientAddGroup.nhds_eq :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G]
(N : AddSubgroup G) (x : G), nhds ↑x = Filter.map QuotientAddGroup.mk (nhds x)
This theorem states that for any type `G` that has a topological space structure, an addition group structure, and is also a topological addition group, given any addition subgroup `N` of `G` and any element `x` of `G`, the neighborhood filter of the quotient of `x` (i.e., the set of all neighborhoods of `x` after considering the equivalent relation induced by `N`) is equal to the map of the neighborhood filter of `x` in the original space `G` under the canonical map to the quotient space. This essentially means that the concept of "closeness" or "neighborhoods" gets carried over appropriately from the original space to the quotient space under the quotient map.
More concisely: For any topological additive group `G` with subgroup `N`, the neighborhood filter of `x` in `G/N` under quotient topology equals the image of `x`'s neighborhood filter in `G` under the quotient map.
|
Filter.Tendsto.const_sub
theorem Filter.Tendsto.const_sub :
∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G] (b : G) {c : G}
{f : α → G} {l : Filter α}, Filter.Tendsto f l (nhds c) → Filter.Tendsto (fun k => b - f k) l (nhds (b - c))
This theorem, `Filter.Tendsto.const_sub`, states that for any types `G` and `α` where `G` is a topological space and subtraction is defined and continuous on `G`, and any elements `b` and `c` of `G`, if a function `f` from `α` to `G` tends to `c` with respect to some filter `l`, then the function which subtracts the value of `f` from the constant `b` also tends to `b - c` with respect to the same filter `l`. In other words, if the limit of function `f` as it approaches the filter `l` is `c`, then the limit of the function `(b - f)` as it approaches `l` is `(b - c)`.
More concisely: If `f: α → G` tends to `c` in the topological space `G` with respect to filter `l`, then the function `(b → b - f(x))` tends to `(b - c)` in `G` with respect to `l`, where `b` is a constant element of `G`.
|