LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31

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.

Left and right translations and inversion in a topological group are homeomorphisms

Statement

For $g$ in a topological group, $L_{g} (x) = g x$ , $R_{g} (x) = x g$ , and $ι (x) = x^{- 1}$ are homeomorphisms.

Facts & Assumptions

Given: A topological group $G$ and $g \in G$ .

[L1]

Multiplication and inversion are continuous (Topological group: multiplication and inversion are continuous).

[L2]

$(g h)^{- 1} = h^{- 1} g^{- 1}$ and inversion is its own inverse (In a group $e^{- 1} = e$ , $(g^{- 1})^{- 1} = g$ and $(g h)^{- 1} = h^{- 1} g^{- 1}$ , the order of the last product being essential).

[L3]

A homeomorphism is a continuous bijection with continuous inverse (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

Proof

technique · direct

1.1

The maps $L_{g}$ and $R_{g}$ are continuous as composites of multiplication with constant maps, and their inverses are $L_{g^{- 1}}$ and $R_{g^{- 1}}$ , also continuous.

L1L2

1.2

Inversion is continuous and its own continuous inverse by [L1] and [L2].

L1L2

2.1

Thus all three maps are homeomorphisms by [L3].

step 1.1step 1.2L3∎

Depends on

Used by

The left and right uniformities of a topological group induce its topology, and inversion interchanges them Theorem

Dependency tree · two levels

13 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

M. Megrelishvili, Lecture Notes in Topological Groups (standard reference, not scraped)