CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Connected Lie subgroups with the same Lie algebra are equal as immersed subgroups

Statement

Assume ${A C}_{ω}$ . Two connected immersed Lie subgroups of a Lie group $G$ with the same tangent Lie subalgebra have the same image and the same intrinsic immersed-subgroup structure: there is a unique Lie-group isomorphism between them commuting with their inclusions into $G$ .

Facts & Assumptions

Given: ${A C}_{ω}$ and connected immersed Lie subgroups $i_{1} : H_{1} \to G$ and $i_{2} : H_{2} \to G$ with the same tangent image $h \subseteq Lie (G)$ .

[F1]

A Lie subalgebra integrates to a connected immersed subgroup uniquely up to the unique isomorphism over $G$ . Lie subgroup–Lie subalgebra correspondence.

Proof

technique · direct

1.1

Apply [F1] to the common subalgebra $h$ . Its uniqueness clause supplies a Lie-group isomorphism $ϕ : H_{1} \to H_{2}$ satisfying $i_{2} \circ ϕ = i_{1}$ .

F1given

2.1

The equality $i_{2} \circ ϕ = i_{1}$ gives $i_{1} (H_{1}) = i_{2} (H_{2})$ as subsets of $G$ . Because $ϕ$ and $ϕ^{- 1}$ are smooth, they identify the intrinsic manifold structures, not merely the underlying image. The zero-dimensional and full-dimensional cases are included, and the stated countable-choice assumption is exactly the one inherited from [F1].

F1step 1.1algebra∎

Depends on

Lie subgroup–Lie subalgebra correspondence

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)