LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pass

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.

Realification preserves a complex norm and its metric

Statement

Let $(V, N)$ be a complex normed space and define $d_{N} (u, v) : = N (u - v)$ for $u, v \in V$ . On the realification $V_{R}$ , the same function $N$ is a real norm. The underlying set, addition, norm values, and induced metric $d_{N}$ are unchanged.

Facts & Assumptions

Given: A complex normed space $(V, N)$ and its realification $V_{R}$ . For each $r \in R$ , write $λ_{r}$ for its canonical complex image.

[F1]

$N : V \to R$ separates zero, is homogeneous for every complex scalar by the complex modulus, and satisfies the triangle inequality (Complex norm and complex normed space).

[F2]

Realification has the same underlying set and addition, and its real scalar action is the complex scalar action restricted along the canonical real embedding (Realification of a complex vector space by restriction of scalars).

[F3]

For every real $r$ , the complex modulus of its canonical image $λ_{r}$ is $∣ r ∣_{R}$ (Complex modulus restricts to real absolute value).

[F4]

A real norm separates zero, is absolutely homogeneous for real scalars, and satisfies the triangle inequality (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[F5]

The induced real norm metric is the function $d_{N} (u, v) = N (u - v)$ , which is a metric (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

Proof

1.1F1F2

Since realification preserves the set, zero vector, and addition, the separation and triangle conditions in [F1] hold unchanged on $V_{R}$ . The codomain remains $R$ .

2.1F1F2F3F4step 1.1

For $r \in R$ and $v \in V$ , [F2] gives $r \cdot_{V_{R}} v = λ_{r} v$ . Hence [F1] and [F3] give $N (r \cdot_{V_{R}} v) = N (λ_{r} v) = ∣ λ_{r} ∣_{C} N (v) = ∣ r ∣_{R} N (v)$ . Together with step 1.1, this is exactly the real norm criterion [F4].

3.1F2F5step 2.1∎

The set and addition are unchanged by [F2], so additive inverses and differences are unchanged as well. The realified norm's induced metric is therefore $N (u - v)$ by [F5], the same function $d_{N}$ defined in the statement, with the same values on the same pairs.

Depends on

Used by

Dependency tree · two levels

21 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

Tomasz Kochanek, Functional analysis, Lecture 1 (complete five-page lecture notes) (standard reference, not scraped)
M. Winklmeier, Functional Analysis lecture notes (complete 140-page lecture notes) (standard reference, not scraped)