Theorems · Definition · Lie groups

AddSubgroup.addSubgroupOfContinuousAddEquivOfLe

{G : Type u_1} →
  [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → {H K : AddSubgroup G} → H ≤ K → ↥(H.addSubgroupOf 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 addSubgroupOfEquivOfLe upgraded to a ContinuousAddEquiv.

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

AddGroupTopologicalSpace