Additional results on topological groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Two results on topological groups that have been separated out as they require more substantial imports developing either positive compacts or the compact open topology.
Some results about an open set containing the product of two sets in a topological group.
theorem
topological_space.positive_compacts.locally_compact_space_of_add_group
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
[t2_space G]
(K : topological_space.positive_compacts G) :
Every separated topological group in which there exists a compact set with nonempty interior is locally compact.
theorem
topological_space.positive_compacts.locally_compact_space_of_group
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
[t2_space G]
(K : topological_space.positive_compacts G) :
Every separated topological group in which there exists a compact set with nonempty interior is locally compact.
@[protected, instance]
def
quotient_add_group.has_continuous_vadd
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
{Γ : add_subgroup G}
[locally_compact_space G] :
has_continuous_vadd G (G ⧸ Γ)
@[protected, instance]
def
quotient_group.has_continuous_smul
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
{Γ : subgroup G}
[locally_compact_space G] :
has_continuous_smul G (G ⧸ Γ)