@[class]
- to_has_continuous_add : has_continuous_add α
- continuous_neg : continuous (λ (a : α), -a)
A topological (additive) group is a group in which the addition and negation operations are continuous.
Instances
- uniform_add_group.to_topological_add_group
- add_group_with_zero_nhd.topological_add_group
- topological_ring.to_topological_add_group
- normed_top_group
- prod.topological_add_group
- topological_add_group_quotient
- real.topological_add_group
- rat.topological_add_group
- complex.topological_add_group
- tangent_space.topological_add_group
@[class]
- to_has_continuous_mul : has_continuous_mul α
- continuous_inv : continuous (λ (a : α), a⁻¹)
A topological group is a group in which the multiplication and inversion operations are continuous.
theorem
continuous_neg
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α] :
continuous (λ (x : α), -x)
theorem
continuous_inv
{α : Type u}
[topological_space α]
[group α]
[topological_group α] :
continuous (λ (x : α), x⁻¹)
theorem
continuous.inv
{α : Type u}
{β : Type v}
[topological_space α]
[group α]
[topological_group α]
[topological_space β]
{f : β → α} :
continuous f → continuous (λ (x : β), (f x)⁻¹)
theorem
continuous.neg
{α : Type u}
{β : Type v}
[topological_space α]
[add_group α]
[topological_add_group α]
[topological_space β]
{f : β → α} :
continuous f → continuous (λ (x : β), -f x)
theorem
continuous_on_neg
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s : set α} :
continuous_on (λ (x : α), -x) s
theorem
continuous_on_inv
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s : set α} :
continuous_on (λ (x : α), x⁻¹) s
theorem
continuous_on.inv
{α : Type u}
{β : Type v}
[topological_space α]
[group α]
[topological_group α]
[topological_space β]
{f : β → α}
{s : set β} :
continuous_on f s → continuous_on (λ (x : β), (f x)⁻¹) s
theorem
continuous_on.neg
{α : Type u}
{β : Type v}
[topological_space α]
[add_group α]
[topological_add_group α]
[topological_space β]
{f : β → α}
{s : set β} :
continuous_on f s → continuous_on (λ (x : β), -f x) s
theorem
tendsto_inv
{α : Type u_1}
[group α]
[topological_space α]
[topological_group α]
(a : α) :
filter.tendsto (λ (x : α), x⁻¹) (nhds a) (nhds a⁻¹)
theorem
tendsto_neg
{α : Type u_1}
[add_group α]
[topological_space α]
[topological_add_group α]
(a : α) :
filter.tendsto (λ (x : α), -x) (nhds a) (nhds (-a))
theorem
filter.tendsto.inv
{α : Type u}
{β : Type v}
[topological_space α]
[group α]
[topological_group α]
{f : β → α}
{x : filter β}
{a : α} :
filter.tendsto f x (nhds a) → filter.tendsto (λ (x : β), (f x)⁻¹) x (nhds a⁻¹)
If a function converges to a value in a multiplicative topological group, then its inverse
converges to the inverse of this value. For the version in normed fields assuming additionally
that the limit is nonzero, use tendsto.inv'.
theorem
filter.tendsto.neg
{α : Type u}
{β : Type v}
[topological_space α]
[add_group α]
[topological_add_group α]
{f : β → α}
{x : filter β}
{a : α} :
filter.tendsto f x (nhds a) → filter.tendsto (λ (x : β), -f x) x (nhds (-a))
theorem
continuous_at.neg
{α : Type u}
{β : Type v}
[topological_space α]
[add_group α]
[topological_add_group α]
[topological_space β]
{f : β → α}
{x : β} :
continuous_at f x → continuous_at (λ (x : β), -f x) x
theorem
continuous_at.inv
{α : Type u}
{β : Type v}
[topological_space α]
[group α]
[topological_group α]
[topological_space β]
{f : β → α}
{x : β} :
continuous_at f x → continuous_at (λ (x : β), (f x)⁻¹) x
theorem
continuous_within_at.inv
{α : Type u}
{β : Type v}
[topological_space α]
[group α]
[topological_group α]
[topological_space β]
{f : β → α}
{s : set β}
{x : β} :
continuous_within_at f s x → continuous_within_at (λ (x : β), (f x)⁻¹) s x
theorem
continuous_within_at.neg
{α : Type u}
{β : Type v}
[topological_space α]
[add_group α]
[topological_add_group α]
[topological_space β]
{f : β → α}
{s : set β}
{x : β} :
continuous_within_at f s x → continuous_within_at (λ (x : β), -f x) s x
@[instance]
def
prod.topological_group
{α : Type u}
{β : Type v}
[topological_space α]
[group α]
[topological_group α]
[topological_space β]
[group β]
[topological_group β] :
topological_group (α × β)
Equations
@[instance]
def
prod.topological_add_group
{α : Type u}
{β : Type v}
[topological_space α]
[add_group α]
[topological_add_group α]
[topological_space β]
[add_group β]
[topological_add_group β] :
topological_add_group (α × β)
def
homeomorph.mul_left
{α : Type u}
[topological_space α]
[group α]
[topological_group α] :
α → α ≃ₜ α
Equations
- homeomorph.mul_left a = {to_equiv := {to_fun := (equiv.mul_left a).to_fun, inv_fun := (equiv.mul_left a).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.add_left
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α] :
α → α ≃ₜ α
theorem
is_open_map_mul_left
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
(a : α) :
is_open_map (λ (x : α), a * x)
theorem
is_open_map_add_left
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
(a : α) :
is_open_map (λ (x : α), a + x)
theorem
is_closed_map_mul_left
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
(a : α) :
is_closed_map (λ (x : α), a * x)
theorem
is_closed_map_add_left
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
(a : α) :
is_closed_map (λ (x : α), a + x)
def
homeomorph.mul_right
{α : Type u_1}
[topological_space α]
[group α]
[topological_group α] :
α → α ≃ₜ α
Equations
- homeomorph.mul_right a = {to_equiv := {to_fun := (equiv.mul_right a).to_fun, inv_fun := (equiv.mul_right a).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.add_right
{α : Type u_1}
[topological_space α]
[add_group α]
[topological_add_group α] :
α → α ≃ₜ α
theorem
is_open_map_add_right
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
(a : α) :
is_open_map (λ (x : α), x + a)
theorem
is_open_map_mul_right
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
(a : α) :
is_open_map (λ (x : α), x * a)
theorem
is_closed_map_add_right
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
(a : α) :
is_closed_map (λ (x : α), x + a)
theorem
is_closed_map_mul_right
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
(a : α) :
is_closed_map (λ (x : α), x * a)
def
homeomorph.neg
(α : Type u_1)
[topological_space α]
[add_group α]
[topological_add_group α] :
α ≃ₜ α
Equations
- homeomorph.inv α = {to_equiv := {to_fun := (equiv.inv α).to_fun, inv_fun := (equiv.inv α).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
exists_nhds_split
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s : set α} :
theorem
exists_nhds_half
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s : set α} :
theorem
nhds_one_symm
(α : Type u)
[topological_space α]
[group α]
[topological_group α] :
filter.comap (λ (r : α), r⁻¹) (nhds 1) = nhds 1
theorem
nhds_zero_symm
(α : Type u)
[topological_space α]
[add_group α]
[topological_add_group α] :
filter.comap (λ (r : α), -r) (nhds 0) = nhds 0
theorem
nhds_translation_mul_inv
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
(x : α) :
theorem
nhds_translation_add_neg
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
(x : α) :
theorem
topological_group.ext
{G : Type u_1}
[group G]
{t t' : topological_space G} :
topological_group G → topological_group G → nhds 1 = nhds 1 → t = t'
theorem
topological_add_group.ext
{G : Type u_1}
[add_group G]
{t t' : topological_space G} :
topological_add_group G → topological_add_group G → nhds 0 = nhds 0 → t = t'
@[instance]
def
quotient_group.quotient.topological_space
{α : Type u}
[group α]
[topological_space α]
(N : subgroup α) :
@[instance]
def
quotient_add_group.quotient.topological_space
{α : Type u}
[add_group α]
[topological_space α]
(N : add_subgroup α) :
theorem
quotient_add_group.open_coe
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
(N : add_subgroup α) :
theorem
quotient_group.open_coe
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
(N : subgroup α) :
@[instance]
def
topological_add_group_quotient
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
(N : add_subgroup α)
(n : N.normal) :
@[instance]
def
topological_group_quotient
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
(N : subgroup α)
(n : N.normal) :
Equations
- _ = _
theorem
continuous.sub
{α : Type u}
{β : Type v}
[topological_space α]
[add_group α]
[topological_add_group α]
[topological_space β]
{f g : β → α} :
continuous f → continuous g → continuous (λ (x : β), f x - g x)
theorem
continuous_sub
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α] :
continuous (λ (p : α × α), p.fst - p.snd)
theorem
continuous_on.sub
{α : Type u}
{β : Type v}
[topological_space α]
[add_group α]
[topological_add_group α]
[topological_space β]
{f g : β → α}
{s : set β} :
continuous_on f s → continuous_on g s → continuous_on (λ (x : β), f x - g x) s
theorem
filter.tendsto.sub
{α : Type u}
{β : Type v}
[topological_space α]
[add_group α]
[topological_add_group α]
{f g : β → α}
{x : filter β}
{a b : α} :
filter.tendsto f x (nhds a) → filter.tendsto g x (nhds b) → filter.tendsto (λ (x : β), f x - g x) x (nhds (a - b))
theorem
nhds_translation
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
(x : α) :
filter.comap (λ (y : α), y - x) (nhds 0) = nhds x
@[class]
- to_add_comm_group : add_comm_group α
- Z : filter α
- zero_Z : has_pure.pure 0 ≤ add_group_with_zero_nhd.Z α
- sub_Z : filter.tendsto (λ (p : α × α), p.fst - p.snd) ((add_group_with_zero_nhd.Z α).prod (add_group_with_zero_nhd.Z α)) (add_group_with_zero_nhd.Z α)
additive group with a neighbourhood around 0. Only used to construct a topology and uniform space.
This is currently only available for commutative groups, but it can be extended to non-commutative groups too.
@[instance]
Equations
- add_group_with_zero_nhd.topological_space α = topological_space.mk_of_nhds (λ (a : α), filter.map (λ (x : α), x + a) (add_group_with_zero_nhd.Z α))
theorem
add_group_with_zero_nhd.neg_Z
{α : Type u}
[add_group_with_zero_nhd α] :
filter.tendsto (λ (a : α), -a) (add_group_with_zero_nhd.Z α) (add_group_with_zero_nhd.Z α)
theorem
add_group_with_zero_nhd.add_Z
{α : Type u}
[add_group_with_zero_nhd α] :
filter.tendsto (λ (p : α × α), p.fst + p.snd) ((add_group_with_zero_nhd.Z α).prod (add_group_with_zero_nhd.Z α)) (add_group_with_zero_nhd.Z α)
theorem
add_group_with_zero_nhd.exists_Z_half
{α : Type u}
[add_group_with_zero_nhd α]
{s : set α} :
s ∈ add_group_with_zero_nhd.Z α → (∃ (V : set α) (H : V ∈ add_group_with_zero_nhd.Z α), ∀ (v : α), v ∈ V → ∀ (w : α), w ∈ V → v + w ∈ s)
theorem
add_group_with_zero_nhd.nhds_eq
{α : Type u}
[add_group_with_zero_nhd α]
(a : α) :
nhds a = filter.map (λ (x : α), x + a) (add_group_with_zero_nhd.Z α)
@[instance]
Equations
@[instance]
Equations
theorem
is_open_add_left
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s t : set α} :
theorem
is_open_mul_left
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s t : set α} :
theorem
is_open_mul_right
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s t : set α} :
theorem
is_open_add_right
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s t : set α} :
theorem
topological_group.t1_space
(α : Type u)
[topological_space α]
[group α]
[topological_group α] :
theorem
topological_group.regular_space
(α : Type u)
[topological_space α]
[group α]
[topological_group α]
[t1_space α] :
theorem
topological_group.t2_space
(α : Type u)
[topological_space α]
[group α]
[topological_group α]
[t1_space α] :
t2_space α
Some results about an open set containing the product of two sets in a topological group.
theorem
zero_open_separated_add
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{U : set α} :
Given a open neighborhood U of 0 there is a open neighborhood V of 0
such that V + V ⊆ U.
theorem
one_open_separated_mul
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{U : set α} :
Given a open neighborhood U of 1 there is a open neighborhood V of 1
such that VV ⊆ U.
theorem
compact_open_separated_add
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{K U : set α} :
Given a compact set K inside an open set U, there is a open neighborhood V of 0
such that K + V ⊆ U.
theorem
compact_open_separated_mul
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{K U : set α} :
Given a compact set K inside an open set U, there is a open neighborhood V of 1
such that KV ⊆ U.
theorem
compact_covered_by_mul_left_translates
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{K V : set α} :
A compact set is covered by finitely many left multiplicative translates of a set with non-empty interior.
theorem
compact_covered_by_add_left_translates
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{K V : set α} :
A compact set is covered by finitely many left additive translates of a set with non-empty interior.
theorem
nhds_add
{α : Type u}
[topological_space α]
[add_comm_group α]
[topological_add_group α]
(x y : α) :
theorem
nhds_mul
{α : Type u}
[topological_space α]
[comm_group α]
[topological_group α]
(x y : α) :
theorem
nhds_is_add_hom
{α : Type u}
[topological_space α]
[add_comm_group α]
[topological_add_group α] :
is_add_hom (λ (x : α), nhds x)
theorem
nhds_is_mul_hom
{α : Type u}
[topological_space α]
[comm_group α]
[topological_group α] :
is_mul_hom (λ (x : α), nhds x)