Theorems · Definition · Lie groups

Subgroup.subgroupOfContinuousMulEquivOfLe

{G : Type u_1} →
  [inst : Group G] → [inst_1 : TopologicalSpace G] → {H K : Subgroup G} → H ≤ K → ↥(H.subgroupOf K) ≃ₜ* ↥H

If G has a topology, and H ≤ K are subgroups, then H as a subgroup of K is isomorphic, as a topological group, to H as a subgroup of G. This is subgroupOfEquivOfLe upgraded to a ContinuousMulEquiv.

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Cited by

4 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpace